---

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


1. e : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. p : Point
6. z : Point
7. u : Point
8. u ≠ p
9. q : Point
10. Colinear(u;z;p)
11. xy  ⊥u uz
12. z # xy
13. z ≠ p
14. zp  ⊥p qp
15. q # zp
16. sep : p ≠ q
17. a : Point
18. b : Point
19. c : Point
20. d : Point
21. v : Point
22. sab : a ≠ b
23. scd : c ≠ d
24. <p, q, sep> = <a, b, sab> ∈ (l,m:Line//l ≡ m)
25. <p, q, sep> ∈ Line
26. <a, b, sab> ∈ Line
27. <p, q, sep> ≡ <a, b, sab>
28. a-v-b
29. c-v-d
30. a leftof cd
31. b leftof dc
32. c leftof ba
33. d leftof ab
34. Colinear(p;q;a)
35. Colinear(p;q;b)
36. Colinear(p;q;a) ∧ Colinear(p;q;b)
⊢ istype((<x, y, l2> ∈ Line) ∧ (<c, d, scd> ∈ Line) ∧ <x, y, l2> ≡ <c, d, scd>)
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  x  :  Point
3.  y  :  Point
4.  l2  :  x  \mneq{}  y
5.  p  :  Point
6.  z  :  Point
7.  u  :  Point
8.  u  \mneq{}  p
9.  q  :  Point
10.  Colinear(u;z;p)
11.  xy    \mbot{}u  uz
12.  z  \#  xy
13.  z  \mneq{}  p
14.  zp    \mbot{}p  qp
15.  q  \#  zp
16.  sep  :  p  \mneq{}  q
17.  a  :  Point
18.  b  :  Point
19.  c  :  Point
20.  d  :  Point
21.  v  :  Point
22.  sab  :  a  \mneq{}  b
23.  scd  :  c  \mneq{}  d
24.  <p,  q,  sep>  =  <a,  b,  sab>
25.  <p,  q,  sep>  \mmember{}  Line
26.  <a,  b,  sab>  \mmember{}  Line
27.  <p,  q,  sep>  \mequiv{}  <a,  b,  sab>
28.  a-v-b
29.  c-v-d
30.  a  leftof  cd
31.  b  leftof  dc
32.  c  leftof  ba
33.  d  leftof  ab
34.  Colinear(p;q;a)
35.  Colinear(p;q;b)
36.  Colinear(p;q;a)  \mwedge{}  Colinear(p;q;b)
\mvdash{}  istype((<x,  y,  l2>  \mmember{}  Line)  \mwedge{}  (<c,  d,  scd>  \mmember{}  Line)  \mwedge{}  <x,  y,  l2>  \mequiv{}  <c,  d,  scd>)


By

---

Latex:
Auto

---

Home Index