---

Step * of Lemma eu-colinear-cycle

∀e:EuclideanPlane. ∀a,b,c:Point.  ((¬(c = a ∈ Point)) ⇒ Colinear(a;b;c) ⇒ Colinear(c;a;b))
BY
{ (Auto
   THEN (All (RWO "eu-colinear-def") THENA Auto)
   THEN ExRepD
   THEN D 0
   THEN Try (Trivial)
   THEN ParallelLast
   THEN Auto) }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. ¬(c = a ∈ Point)@i
6. ¬(a = b ∈ Point)
7. ¬(b = c ∈ Point)@i
8. ¬(b = a ∈ Point)@i
9. ¬b-c-a@i
10. ¬c-b-a@i
11. ¬c-a-b@i
12. ¬(c = a ∈ Point)
13. ¬(c = b ∈ Point)
14. ¬c-a-b
⊢ ¬a-c-b

2
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. ¬(c = a ∈ Point)@i
6. ¬(a = b ∈ Point)
7. ¬(b = c ∈ Point)@i
8. ¬(b = a ∈ Point)@i
9. ¬b-c-a@i
10. ¬c-b-a@i
11. ¬c-a-b@i
12. ¬(c = a ∈ Point)
13. ¬(c = b ∈ Point)
14. ¬c-a-b
15. ¬a-c-b
⊢ ¬a-b-c

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    ((\mneg{}(c  =  a))  {}\mRightarrow{}  Colinear(a;b;c)  {}\mRightarrow{}  Colinear(c;a;b))


By

---

Latex:
(Auto
  THEN  (All  (RWO  "eu-colinear-def")  THENA  Auto)
  THEN  ExRepD
  THEN  D  0
  THEN  Try  (Trivial)
  THEN  ParallelLast
  THEN  Auto)

---

Home Index