---

Step * of Lemma geo-gt-sep

∀e:EuclideanPlane. ∀A,B,C,P:Point.  (AB > CP ⇒ A ≠ B)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `geo-gt` -1
   THEN ((((D -1 THENA Auto) THEN Unhide) THENA Auto) THEN ExRepD)
   THEN InstLemma `geo-between-sep` [⌜e⌝;⌜B⌝;⌜A⌝;⌜w⌝] ⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C,P:Point.    (AB  >  CP  {}\mRightarrow{}  A  \mneq{}  B)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `geo-gt`  -1
  THEN  ((((D  -1  THENA  Auto)  THEN  Unhide)  THENA  Auto)  THEN  ExRepD)
  THEN  InstLemma  `geo-between-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]  \mcdot{}
  THEN  EAuto  1)

---

Home Index