---

Step * 1 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. u : Point
7. q : Point
8. Colinear(p;z;p)
9. ab  ⊥p pz
10. z # ab
11. z # p
12. zp  ⊥p qp
13. q # zp
14. a # b
15. p # q
16. u ≡ p
17. ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof pq ∧ y leftof qp)
⊢ False
BY
{ (ThinVar `u' THEN Thin (-7)) }

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)
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
(ThinVar  `u'  THEN  Thin  (-7))

---

Home Index