---

Step * of Lemma not-col-distincts

∀e:BasicGeometry. ∀A,B,C:Point.  ((¬Colinear(A;B;C)) ⇒ (¬¬(A ≠ B ∧ B ≠ C ∧ A ≠ C)))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (gSeparatedCases ⌜A⌝ ⌜B⌝⋅ THEN Auto)
   THEN (gSeparatedCases ⌜B⌝ ⌜C⌝⋅ THEN Auto)
   THEN gSeparatedCases ⌜A⌝ ⌜C⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,C:Point.    ((\mneg{}Colinear(A;B;C))  {}\mRightarrow{}  (\mneg{}\mneg{}(A  \mneq{}  B  \mwedge{}  B  \mneq{}  C  \mwedge{}  A  \mneq{}  C)))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (gSeparatedCases  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (gSeparatedCases  \mkleeneopen{}B\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  gSeparatedCases  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index