---

Step * 1 1 2 1 2 1 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)
16. Colinear(a;b;p)
⊢ False
BY
{ ((ExRepD THEN (Assert Colinear(x;p;q) BY (D 14 THEN Unhide THEN Auto))) THEN Unfold `geo-colinear` -1 THEN Auto) }

---

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)
16.  Colinear(a;b;p)
\mvdash{}  False


By

---

Latex:
((ExRepD  THEN  (Assert  Colinear(x;p;q)  BY  (D  14  THEN  Unhide  THEN  Auto)))
  THEN  Unfold  `geo-colinear`  -1
  THEN  Auto)

---

Home Index