---

Step * of Lemma geo-colinear-from-between

∀e:BasicGeometry. ∀[A,C,D:Point].  (A ≠ C ⇒ (∃B:Point. (A ≠ B ∧ A_C_B ∧ A_D_B)) ⇒ Colinear(A;C;D))
BY
{ (Auto THEN ExRepD THEN InstLemma `geo-colinear-between` [⌜e⌝;⌜A⌝;⌜B⌝;⌜C⌝;⌜D⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[A,C,D:Point].    (A  \mneq{}  C  {}\mRightarrow{}  (\mexists{}B:Point.  (A  \mneq{}  B  \mwedge{}  A\_C\_B  \mwedge{}  A\_D\_B))  {}\mRightarrow{}  Colinear(A;C;D))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  InstLemma  `geo-colinear-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index