---

Step * 2 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. abc ≅a abd
⊢ Rabc
BY
{ (D -1 THEN ExRepD) }

1
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_x'
19. b_d_z'
20. ba' ≅ bx'
21. bc' ≅ bz'
22. a'c' ≅ x'z'
⊢ 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.  abc  \mcong{}\msuba{}  abd
\mvdash{}  Rabc


By

---

Latex:
(D  -1  THEN  ExRepD)

---

Home Index