---

Step * 2 of Lemma eu-colinear-swap


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
BY
{ (ParallelOp 9 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  a  :  Point@i
3.  b  :  Point@i
4.  c  :  Point@i
5.  \mneg{}(a  =  b)
6.  \mneg{}(c  =  b)@i
7.  \mneg{}(c  =  a)@i
8.  \mneg{}c-b-a@i
9.  \mneg{}b-c-a@i
10.  \mneg{}b-a-c@i
11.  \mneg{}(c  =  a)
12.  \mneg{}(c  =  b)
13.  \mneg{}c-a-b
\mvdash{}  \mneg{}a-c-b


By

---

Latex:
(ParallelOp  9  THEN  EAuto  1)

---

Home Index