---

Step * of Lemma geo-playfair-axiom

∀e:EuclideanParPlane. ∀p:Point. ∀l,m,n:Line.  ((p I m ∧ m || l) ⇒ (p I n ∧ n || l) ⇒ m ≡ n)
BY
{ ((Fold `Playfair-axiom` 0 THEN Auto) THEN D 1 THEN Unhide THEN EAuto 2) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}p:Point.  \mforall{}l,m,n:Line.    ((p  I  m  \mwedge{}  m  ||  l)  {}\mRightarrow{}  (p  I  n  \mwedge{}  n  ||  l)  {}\mRightarrow{}  m  \mequiv{}  n)


By

---

Latex:
((Fold  `Playfair-axiom`  0  THEN  Auto)  THEN  D  1  THEN  Unhide  THEN  EAuto  2)

---

Home Index