---

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

.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. p : Point
5. z : Point
6. u : Point
7. q : Point
8. Colinear(u;z;p)
9. ab  ⊥u uz
10. z # ab
11. z # p
12. zp  ⊥p qp
13. q # zp
14. a # b
15. p # q
16. u # p
17. x : {z:Point| Colinear(z;a;b)} 
18. y : {z:Point| Colinear(z;a;b)} 
19. x leftof pq
20. y leftof qp
21. a # b
22. p # q
23. a1 : Point
24. b1 : Point
25. c : Point
26. d : Point
27. v : Point
28. a1-v-b1
29. c-v-d
30. Colinear(a1;a;b)
31. Colinear(b1;a;b)
32. Colinear(c;p;q)
33. Colinear(d;p;q)
34. a1 leftof cd
35. b1 leftof dc
36. c leftof b1a1
37. d leftof a1b1
⊢ Rvpu
BY
{ (Assert Rupv BY
         Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. p : Point
5. z : Point
6. u : Point
7. q : Point
8. Colinear(u;z;p)
9. ab  ⊥u uz
10. z # ab
11. z # p
12. zp  ⊥p qp
13. q # zp
14. a # b
15. p # q
16. u # p
17. x : {z:Point| Colinear(z;a;b)} 
18. y : {z:Point| Colinear(z;a;b)} 
19. x leftof pq
20. y leftof qp
21. a # b
22. p # q
23. a1 : Point
24. b1 : Point
25. c : Point
26. d : Point
27. v : Point
28. a1-v-b1
29. c-v-d
30. Colinear(a1;a;b)
31. Colinear(b1;a;b)
32. Colinear(c;p;q)
33. Colinear(d;p;q)
34. a1 leftof cd
35. b1 leftof dc
36. c leftof b1a1
37. d leftof a1b1
38. Rupv
⊢ Rvpu

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  \{b:Point|  a  \#  b\} 
4.  p  :  Point
5.  z  :  Point
6.  u  :  Point
7.  q  :  Point
8.  Colinear(u;z;p)
9.  ab    \mbot{}u  uz
10.  z  \#  ab
11.  z  \#  p
12.  zp    \mbot{}p  qp
13.  q  \#  zp
14.  a  \#  b
15.  p  \#  q
16.  u  \#  p
17.  x  :  \{z:Point|  Colinear(z;a;b)\} 
18.  y  :  \{z:Point|  Colinear(z;a;b)\} 
19.  x  leftof  pq
20.  y  leftof  qp
21.  a  \#  b
22.  p  \#  q
23.  a1  :  Point
24.  b1  :  Point
25.  c  :  Point
26.  d  :  Point
27.  v  :  Point
28.  a1-v-b1
29.  c-v-d
30.  Colinear(a1;a;b)
31.  Colinear(b1;a;b)
32.  Colinear(c;p;q)
33.  Colinear(d;p;q)
34.  a1  leftof  cd
35.  b1  leftof  dc
36.  c  leftof  b1a1
37.  d  leftof  a1b1
\mvdash{}  Rvpu


By

---

Latex:
(Assert  Rupv  BY
              Auto)

---

Home Index