---

Step * of Lemma not-geo-triangle-iff-colinear

∀e:HeytingGeometry. ∀a,b,c:Point.  (¬a # bc ⇐⇒ Colinear(a;b;c))
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma `euclidean-plane-axioms` [⌜e⌝]⋅ THENA Auto)
   THEN Unfold `geo-triangle` 0
   THEN SplitAndHyps
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.    (\mneg{}a  \#  bc  \mLeftarrow{}{}\mRightarrow{}  Colinear(a;b;c))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `euclidean-plane-axioms`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `geo-triangle`  0
  THEN  SplitAndHyps
  THEN  Trivial)

---

Home Index