---

Step * of Lemma geo-congruent-sep

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab ≅ cd ⇒ c # d ⇒ a # b)
BY
{ (Auto THEN InstLemma `geo-ge-sep` [⌜e⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab ≅ cd
7. c # d
⊢ ab ≥ cd

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab  \mcong{}  cd  {}\mRightarrow{}  c  \#  d  {}\mRightarrow{}  a  \#  b)


By

---

Latex:
(Auto  THEN  InstLemma  `geo-ge-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index