---

Step * of Lemma eu-colinear-permute

∀e:EuclideanPlane. ∀a,b,c:Point.  ((¬(c = b ∈ Point)) ⇒ Colinear(a;b;c) ⇒ Colinear(c;b;a))
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 = b ∈ Point)@i
6. ¬(a = b ∈ Point)
7. ¬(a = c ∈ Point)@i
8. ¬(a = b ∈ Point)@i
9. ¬a-c-b@i
10. ¬c-a-b@i
11. ¬c-b-a@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  =  b))  {}\mRightarrow{}  Colinear(a;b;c)  {}\mRightarrow{}  Colinear(c;b;a))


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