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


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

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

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


By


Latex:
Assert  \mkleeneopen{}Colinear(a;b;q)\mkleeneclose{}\mcdot{}




Home Index