---

Step * 1 1 2 1 2 of Lemma Euclid-parallel-points-exists


1. e : EuclideanPlane
2. p : Point
3. a : Point
4. b : {b:Point| a # b} 
5. z : Point
6. q : Point
7. Colinear(p;z;p)
8. ab  ⊥p pz
9. z # p
10. zp  ⊥p qp
11. q # zp
12. a # b
13. p # q
14. ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof pq ∧ y leftof qp)
15. Colinear(a;b;q)
⊢ False
BY
{ (Assert Colinear(a;b;p) BY
         Auto) }

1
1. e : EuclideanPlane
2. p : Point
3. a : Point
4. b : {b:Point| a # b} 
5. z : Point
6. q : Point
7. Colinear(p;z;p)
8. ab  ⊥p pz
9. z # p
10. zp  ⊥p qp
11. q # zp
12. a # b
13. p # q
14. ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof pq ∧ y leftof qp)
15. Colinear(a;b;q)
16. Colinear(a;b;p)
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Point
3.  a  :  Point
4.  b  :  \{b:Point|  a  \#  b\} 
5.  z  :  Point
6.  q  :  Point
7.  Colinear(p;z;p)
8.  ab    \mbot{}p  pz
9.  z  \#  p
10.  zp    \mbot{}p  qp
11.  q  \#  zp
12.  a  \#  b
13.  p  \#  q
14.  \mexists{}x,y:\{z:Point|  Colinear(z;a;b)\}  .  (x  leftof  pq  \mwedge{}  y  leftof  qp)
15.  Colinear(a;b;q)
\mvdash{}  False


By

---

Latex:
(Assert  Colinear(a;b;p)  BY
              Auto)

---

Home Index