---

Step * of Lemma eu-between-eq-implies-colinear3

∀e:EuclideanPlane. ∀[a,b,c:Point].  (Colinear(a;b;c)) supposing (b_c_a and (¬(a = b ∈ Point)))
BY
{ (Auto
   THEN EuContradiction
   THEN (RWO  "eu-between-eq-def" (-2) THENA Auto)
   THEN (RWO  "eu-colinear-def" (-1) THENA Auto)) }

1
1. e : EuclideanPlane@i'
2. a : Point
3. b : Point
4. c : Point
5. ¬(a = b ∈ Point)
6. ¬((¬(b = c ∈ Point)) ∧ (¬(a = c ∈ Point)) ∧ (¬b-c-a))
7. ¬((¬(a = b ∈ Point)) ∧ (¬((¬(c = a ∈ Point)) ∧ (¬(c = b ∈ Point)) ∧ (¬c-a-b) ∧ (¬a-c-b) ∧ (¬a-b-c))))@i
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c:Point].    (Colinear(a;b;c))  supposing  (b\_c\_a  and  (\mneg{}(a  =  b)))


By

---

Latex:
(Auto
  THEN  EuContradiction
  THEN  (RWO    "eu-between-eq-def"  (-2)  THENA  Auto)
  THEN  (RWO    "eu-colinear-def"  (-1)  THENA  Auto))

---

Home Index