---

Step * 1 of Lemma eu-colinear-permute


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

---

Latex:

---

Latex:

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


By

---

Latex:
(ParallelOp  11  THEN  EAuto  1)

---

Home Index