---

Step * 1 of Lemma sup-angles-preserve-congruence


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. x' : Point
10. abc ≅a xyz
11. a # bc
12. x # yz
13. a-b-a'
14. x-y-x'
15. a1 : Point
16. c' : Point
17. x1 : Point
18. z' : Point
19. out(b a1a)
20. out(b c'c)
21. out(y x1x)
22. out(y z'z)
23. a1bc' ≅a x1yz'
24. Cong3(a1bc',x1yz')
25. A : Point
26. b-a'-A
27. a'A ≅ yx'
28. X : Point
29. y-x'-X
30. x'X ≅ ba'
31. a1_b_A
32. x1_y_X
33. bA ≅ yX
⊢ a'bc ≅a x'yz
BY
{ (InstLemma `geo-five-segment` [⌜e⌝;⌜a1⌝;⌜b⌝;⌜A⌝;⌜c'⌝;⌜x1⌝;⌜y⌝;⌜X⌝;⌜z'⌝]⋅ THENA (D 24 THEN Auto)) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. x' : Point
10. abc ≅a xyz
11. a # bc
12. x # yz
13. a-b-a'
14. x-y-x'
15. a1 : Point
16. c' : Point
17. x1 : Point
18. z' : Point
19. out(b a1a)
20. out(b c'c)
21. out(y x1x)
22. out(y z'z)
23. a1bc' ≅a x1yz'
24. Cong3(a1bc',x1yz')
25. A : Point
26. b-a'-A
27. a'A ≅ yx'
28. X : Point
29. y-x'-X
30. x'X ≅ ba'
31. a1_b_A
32. x1_y_X
33. bA ≅ yX
34. Ac' ≅ Xz'
⊢ a'bc ≅a x'yz

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  a'  :  Point
9.  x'  :  Point
10.  abc  \00D0\msuba{}  xyz
11.  a  \#  bc
12.  x  \#  yz
13.  a-b-a'
14.  x-y-x'
15.  a1  :  Point
16.  c'  :  Point
17.  x1  :  Point
18.  z'  :  Point
19.  out(b  a1a)
20.  out(b  c'c)
21.  out(y  x1x)
22.  out(y  z'z)
23.  a1bc'  \00D0\msuba{}  x1yz'
24.  Cong3(a1bc',x1yz')
25.  A  :  Point
26.  b-a'-A
27.  a'A  \00D0  yx'
28.  X  :  Point
29.  y-x'-X
30.  x'X  \00D0  ba'
31.  a1\_b\_A
32.  x1\_y\_X
33.  bA  \00D0  yX
\mvdash{}  a'bc  \00D0\msuba{}  x'yz


By

---

Latex:
(InstLemma  `geo-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}  THENA  (D  24  THEN  Auto))

---

Home Index