---

Step * of Lemma eu-colinear-swap

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

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

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

---

Latex:

---

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


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