---

Step * of Lemma upper-dimension-axiom

∀g:EuclideanPlane. ∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ Colinear(a;b;c))
BY
{ ((D 0 THENA Auto)
   THEN (Assert BasicGeometryAxioms(g) BY
               (D 1 THEN Unhide THEN Auto))
   THEN (D -1 THEN SplitAndHyps)
   THEN Unfold `geo-colinear` 0
   THEN Hypothesis) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,x,y:Point.    (ax  \mcong{}  ay  {}\mRightarrow{}  bx  \mcong{}  by  {}\mRightarrow{}  cx  \mcong{}  cy  {}\mRightarrow{}  x  \#  y  {}\mRightarrow{}  Colinear(a;b;c))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  BasicGeometryAxioms(g)  BY
                          (D  1  THEN  Unhide  THEN  Auto))
  THEN  (D  -1  THEN  SplitAndHyps)
  THEN  Unfold  `geo-colinear`  0
  THEN  Hypothesis)

---

Home Index