---

Step * 1 of Lemma stable__Playfair-axiom


1. g : EuclideanPlane
⊢ Stable{∀p:Point. ∀l,m,n:Line.  ((p I m ∧ m || l) ⇒ (p I n ∧ n || l) ⇒ m ≡ n)}
BY
{ (RepeatFor 4 ((BLemma `stable__all` THEN Auto)) THEN RepeatFor 2 ((BLemma `stable__implies` THEN Auto))) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
\mvdash{}  Stable\{\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:
(RepeatFor  4  ((BLemma  `stable\_\_all`  THEN  Auto))
  THEN  RepeatFor  2  ((BLemma  `stable\_\_implies`  THEN  Auto))
  )

---

Home Index