---

Step * 1 1 1 1 1 1 1 1 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. <x, y, l2> = <c, d, scd> ∈ (l,m:Line//l ≡ m)
29. <x, y, l2> ∈ Line
30. <c, d, scd> ∈ Line
31. <x, y, l2> ≡ <c, d, scd>
32. a-v-b
33. c-v-d
34. a leftof cd
35. b leftof dc
36. c leftof ba
37. d leftof ab
38. Colinear(p;q;a)
39. Colinear(p;q;b)
40. Colinear(x;y;c) ∧ Colinear(x;y;d)
⊢ False
BY
{ (InstLemma `right-angles-not-complementary` [⌜e⌝;⌜v⌝;⌜u⌝;⌜p⌝]⋅ THENA Auto) }

1
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. <x, y, l2> = <c, d, scd> ∈ (l,m:Line//l ≡ m)
29. <x, y, l2> ∈ Line
30. <c, d, scd> ∈ Line
31. <x, y, l2> ≡ <c, d, scd>
32. a-v-b
33. c-v-d
34. a leftof cd
35. b leftof dc
36. c leftof ba
37. d leftof ab
38. Colinear(p;q;a)
39. Colinear(p;q;b)
40. Colinear(x;y;c)
41. Colinear(x;y;d)
⊢ Rvpu

2
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. <x, y, l2> = <c, d, scd> ∈ (l,m:Line//l ≡ m)
29. <x, y, l2> ∈ Line
30. <c, d, scd> ∈ Line
31. <x, y, l2> ≡ <c, d, scd>
32. a-v-b
33. c-v-d
34. a leftof cd
35. b leftof dc
36. c leftof ba
37. d leftof ab
38. Colinear(p;q;a)
39. Colinear(p;q;b)
40. Colinear(x;y;c) ∧ Colinear(x;y;d)
41. u ≡ p
⊢ False

---

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.  <x,  y,  l2>  =  <c,  d,  scd>
29.  <x,  y,  l2>  \mmember{}  Line
30.  <c,  d,  scd>  \mmember{}  Line
31.  <x,  y,  l2>  \mequiv{}  <c,  d,  scd>
32.  a-v-b
33.  c-v-d
34.  a  leftof  cd
35.  b  leftof  dc
36.  c  leftof  ba
37.  d  leftof  ab
38.  Colinear(p;q;a)
39.  Colinear(p;q;b)
40.  Colinear(x;y;c)  \mwedge{}  Colinear(x;y;d)
\mvdash{}  False


By

---

Latex:
(InstLemma  `right-angles-not-complementary`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index