Step * 1 of Lemma eu-colinear-swap


1. EuclideanPlane@i'
2. Point@i
3. Point@i
4. 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
BY
(ParallelOp 10 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)
\mvdash{}  \mneg{}c-a-b


By


Latex:
(ParallelOp  10  THEN  EAuto  1)




Home Index