---

Step * 2 of Lemma adjacent-right-angles-supplementary-using-geom-tactic


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 THEN GeometryFor ``geo-congruent geo-eq`` 2) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a ≠ b
8. b ≠ c
9. b ≠ d
10. a' : Point
11. c' : Point
12. z' : Point
13. b_a_a'
14. b_c_c'
15. b_d_z'
16. ba' ≅ ba'
17. bc' ≅ bz'
18. a'c' ≅ a'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  THEN  GeometryFor  ``geo-congruent  geo-eq``  2)

---

Home Index