---

Step * 1 of Lemma eu-colinear-cycle


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
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{}(c  =  a)@i
6.  \mneg{}(a  =  b)
7.  \mneg{}(b  =  c)@i
8.  \mneg{}(b  =  a)@i
9.  \mneg{}b-c-a@i
10.  \mneg{}c-b-a@i
11.  \mneg{}c-a-b@i
12.  \mneg{}(c  =  a)
13.  \mneg{}(c  =  b)
14.  \mneg{}c-a-b
\mvdash{}  \mneg{}a-c-b


By

---

Latex:
(ParallelOp  9  THEN  EAuto  1)

---

Home Index