---

Step * 2 1 1 of Lemma adjacent-right-angles-supplementary


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a ≠ b
8. a ≠ b
9. b ≠ c
10. a ≠ b
11. b ≠ d
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. b_a_a'
17. b_c_c'
18. b_a_a'
19. b_d_z'
20. ba' ≅ ba'
21. bc' ≅ bz'
22. a'c' ≅ a'z'
23. a'a ≅ a'a
24. x' ≡ a'
⊢ Rabc
BY
{ (Assert Ra'bc' BY
         (D 0 THEN Auto)) }

1
.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a ≠ b
8. a ≠ b
9. b ≠ c
10. a ≠ b
11. b ≠ d
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. b_a_a'
17. b_c_c'
18. b_a_a'
19. b_d_z'
20. ba' ≅ ba'
21. bc' ≅ bz'
22. a'c' ≅ a'z'
23. a'a ≅ a'a
24. x' ≡ a'
25. c'@0 : Point
26. c'@0=b=c'
⊢ a'c' ≅ a'c'@0

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a ≠ b
8. a ≠ b
9. b ≠ c
10. a ≠ b
11. b ≠ d
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. b_a_a'
17. b_c_c'
18. b_a_a'
19. b_d_z'
20. ba' ≅ ba'
21. bc' ≅ bz'
22. a'c' ≅ a'z'
23. a'a ≅ a'a
24. x' ≡ a'
25. Ra'bc'
⊢ Rabc

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  c-b-d
7.  a  \mneq{}  b
8.  a  \mneq{}  b
9.  b  \mneq{}  c
10.  a  \mneq{}  b
11.  b  \mneq{}  d
12.  a'  :  Point
13.  c'  :  Point
14.  x'  :  Point
15.  z'  :  Point
16.  b\_a\_a'
17.  b\_c\_c'
18.  b\_a\_a'
19.  b\_d\_z'
20.  ba'  \mcong{}  ba'
21.  bc'  \mcong{}  bz'
22.  a'c'  \mcong{}  a'z'
23.  a'a  \mcong{}  a'a
24.  x'  \mequiv{}  a'
\mvdash{}  Rabc


By

---

Latex:
(Assert  Ra'bc'  BY
              (D  0  THEN  Auto))

---

Home Index