---

Step * of Lemma eu-not-not-colinear

∀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 RWO "eu-colinear-def" 0 THEN Auto) }

1
1. e : EuclideanStructure@i'
2. a : Point
3. b : Point
4. c : Point
5. ¬¬((¬(a = b ∈ Point)) ∧ (¬((¬(c = a ∈ Point)) ∧ (¬(c = b ∈ Point)) ∧ (¬c-a-b) ∧ (¬a-c-b) ∧ (¬a-b-c))))@i
⊢ ¬¬((c = a ∈ Point) ∨ (c = b ∈ Point) ∨ c-a-b ∨ a-c-b ∨ a-b-c)

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "eu-colinear-def"  0  THEN  Auto)

---

Home Index