---

Step * of Lemma eu-between-eq-def

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

---

Latex:

---

Latex:
\mforall{}e:EuclideanStructure.  \mforall{}[a,b,c:Point].    (a\_b\_c  \mLeftarrow{}{}\mRightarrow{}  \mneg{}((\mneg{}(a  =  b))  \mwedge{}  (\mneg{}(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."T"  a  b  c  \mLeftarrow{}{}\mRightarrow{}  \mneg{}((\mneg{}(a  =  b))  \mwedge{}  (\mneg{}(c  =  b))  \mwedge{}  (\mneg{}(e."B"  a  b  c))))  BY
                          (UseWitness  \mkleeneopen{}e."Tdef"\mkleeneclose{}\mcdot{}  THEN  Trivial))
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Unfolds  ``eu-point  eu-between-eq  eu-between  eu-separated``  0\mcdot{}
  THEN  Trivial)

---

Home Index