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