---

Step * 1 1 of Lemma geo-cong-angle-transitivity


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. r : Point
11. a # b
12. c # b
13. x # y
14. z # y
15. p # q
16. r # q
17. a # b
18. b # c
19. x # y
20. y # z
21. a1 : Point
22. c1 : Point
23. x1 : Point
24. z1 : Point
25. B(baa1)
26. B(bcc1)
27. B(yxx1)
28. B(yzz1)
29. ba1 ≅ yx1
30. bc1 ≅ yz1
31. a1c1 ≅ x1z1
32. x # y
33. y # z
34. p # q
35. q # r
36. a' : Point
37. c' : Point
38. x' : Point
39. z' : Point
40. B(yxa')
41. B(yzc')
42. B(qpx')
43. B(qrz')
44. ya' ≅ qx'
45. yc' ≅ qz'
46. a'c' ≅ x'z'
47. A : Point
48. B(ba1A) ∧ a1A ≅ qx'
49. X : Point
50. B(qx'X) ∧ x'X ≅ ba1
51. C : Point
52. B(bc1C) ∧ c1C ≅ qz'
53. Z : Point
54. B(qz'Z) ∧ z'Z ≅ bc1
⊢ ((a # b ∧ b # c) ∧ p # q) ∧ q # r
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  p  :  Point
9.  q  :  Point
10.  r  :  Point
11.  a  \#  b
12.  c  \#  b
13.  x  \#  y
14.  z  \#  y
15.  p  \#  q
16.  r  \#  q
17.  a  \#  b
18.  b  \#  c
19.  x  \#  y
20.  y  \#  z
21.  a1  :  Point
22.  c1  :  Point
23.  x1  :  Point
24.  z1  :  Point
25.  B(baa1)
26.  B(bcc1)
27.  B(yxx1)
28.  B(yzz1)
29.  ba1  \mcong{}  yx1
30.  bc1  \mcong{}  yz1
31.  a1c1  \mcong{}  x1z1
32.  x  \#  y
33.  y  \#  z
34.  p  \#  q
35.  q  \#  r
36.  a'  :  Point
37.  c'  :  Point
38.  x'  :  Point
39.  z'  :  Point
40.  B(yxa')
41.  B(yzc')
42.  B(qpx')
43.  B(qrz')
44.  ya'  \mcong{}  qx'
45.  yc'  \mcong{}  qz'
46.  a'c'  \mcong{}  x'z'
47.  A  :  Point
48.  B(ba1A)  \mwedge{}  a1A  \mcong{}  qx'
49.  X  :  Point
50.  B(qx'X)  \mwedge{}  x'X  \mcong{}  ba1
51.  C  :  Point
52.  B(bc1C)  \mwedge{}  c1C  \mcong{}  qz'
53.  Z  :  Point
54.  B(qz'Z)  \mwedge{}  z'Z  \mcong{}  bc1
\mvdash{}  ((a  \#  b  \mwedge{}  b  \#  c)  \mwedge{}  p  \#  q)  \mwedge{}  q  \#  r


By

---

Latex:
Auto

---

Home Index