---

Step * of Lemma eu-not-colinear-OXY

∀[e:EuclideanStructure]. ((¬(O = X ∈ Point)) ∧ (¬Colinear(O;X;Y)))
BY
{ ((D 0 THENA Auto) THEN Unfolds ``eu-O eu-X eu-Y`` 0 THEN (At ⌜Type⌝ (GenConclTerm ⌜eu-nontrivial(e)⌝)⋅ THENA Auto)) }

1
1. e : EuclideanStructure
2. v : {triple:Point × Point × Point| let a,b,c = triple in (¬(a = b ∈ Point)) ∧ (¬Colinear(a;b;c))} @i
3. eu-nontrivial(e)
= v
∈ {triple:Point × Point × Point| let a,b,c = triple in (¬(a = b ∈ Point)) ∧ (¬Colinear(a;b;c))} @i
⊢ (¬((fst(v)) = (fst(snd(v))) ∈ Point)) ∧ (¬Colinear(fst(v);fst(snd(v));snd(snd(v))))

---

Latex:

---

Latex:
\mforall{}[e:EuclideanStructure].  ((\mneg{}(O  =  X))  \mwedge{}  (\mneg{}Colinear(O;X;Y)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfolds  ``eu-O  eu-X  eu-Y``  0
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (GenConclTerm  \mkleeneopen{}eu-nontrivial(e)\mkleeneclose{})\mcdot{}  THENA  Auto))

---

Home Index