---

Step * of Lemma eu-colinear-def

∀e:EuclideanStructure
  ∀[a,b,c:Point].
    (Colinear(a;b;c)
    ⇐⇒ (¬(a = b ∈ Point)) ∧ (¬((¬(c = a ∈ Point)) ∧ (¬(c = b ∈ Point)) ∧ (¬c-a-b) ∧ (¬a-c-b) ∧ (¬a-b-c))))
BY
{ ((UnivCD THENA Auto)
   THEN (DRecord 1 THENA Auto)
   THEN (Assert ∀[a,b,c:e."Point"].
                  (e."colinear" a b c
                  ⇐⇒ (¬(a = b ∈ e."Point"))
                      ∧ (¬((¬(c = a ∈ e."Point"))
                        ∧ (¬(c = b ∈ e."Point"))
                        ∧ (¬(e."B" c a b))
                        ∧ (¬(e."B" a c b))
                        ∧ (¬(e."B" a b c))))) BY
               (UseWitness ⌜e."colineardef"⌝⋅ THEN Trivial))
   THEN (InstHyp [⌜a⌝;⌜b⌝;⌜c⌝] (-1)⋅ THENA Auto)
   THEN Unfolds ``eu-point eu-colinear eu-between eu-separated`` 0⋅
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanStructure
    \mforall{}[a,b,c:Point].
        (Colinear(a;b;c)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(a  =  b))  \mwedge{}  (\mneg{}((\mneg{}(c  =  a))  \mwedge{}  (\mneg{}(c  =  b))  \mwedge{}  (\mneg{}c-a-b)  \mwedge{}  (\mneg{}a-c-b)  \mwedge{}  (\mneg{}a-b-c))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (DRecord  1  THENA  Auto)
  THEN  (Assert  \mforall{}[a,b,c:e."Point"].
                                (e."colinear"  a  b  c
                                \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(a  =  b))
                                        \mwedge{}  (\mneg{}((\mneg{}(c  =  a))
                                            \mwedge{}  (\mneg{}(c  =  b))
                                            \mwedge{}  (\mneg{}(e."B"  c  a  b))
                                            \mwedge{}  (\mneg{}(e."B"  a  c  b))
                                            \mwedge{}  (\mneg{}(e."B"  a  b  c)))))  BY
                          (UseWitness  \mkleeneopen{}e."colineardef"\mkleeneclose{}\mcdot{}  THEN  Trivial))
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Unfolds  ``eu-point  eu-colinear  eu-between  eu-separated``  0\mcdot{}
  THEN  Trivial)

---

Home Index