---

Step * 1 of Lemma eu-not-colinear-OXY


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))))
BY
{ ((D 0 THENA Auto) THEN RepeatFor 2 (D 2) THEN D 3 THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanStructure
2.  v  :  \{triple:Point  \mtimes{}  Point  \mtimes{}  Point|  let  a,b,c  =  triple  in  (\mneg{}(a  =  b))  \mwedge{}  (\mneg{}Colinear(a;b;c))\}  @i
3.  eu-nontrivial(e)  =  v@i
\mvdash{}  (\mneg{}((fst(v))  =  (fst(snd(v)))))  \mwedge{}  (\mneg{}Colinear(fst(v);fst(snd(v));snd(snd(v))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  RepeatFor  2  (D  2)  THEN  D  3  THEN  All  Reduce  THEN  Auto)

---

Home Index