---

Step * of Lemma geo-parallel-lsep-opp

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (geo-parallel(e;a;b;c;d) ⇒ c # ab)
BY
{ (((Auto THEN D -1) THEN ExRepD)
   THEN (((InstLemma `lsep-iff-all-sep` [⌜e⌝;⌜c⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN D -1) THEN D -1 THEN Auto)
   THEN InstHyp [⌜x⌝] (8)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (geo-parallel(e;a;b;c;d)  {}\mRightarrow{}  c  \#  ab)


By

---

Latex:
(((Auto  THEN  D  -1)  THEN  ExRepD)
  THEN  (((InstLemma  `lsep-iff-all-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)  THEN  D  -1  THEN  Auto)
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (8)\mcdot{}
  THEN  Auto)

---

Home Index