---

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

.....assertion..... 
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'
⊢ Ra'bc'
BY
{ (D 0 THEN Auto THEN (Assert c'=b=z' BY (D 0 THEN Auto)) THEN GeometryFor ``geo-midpoint geo-eq`` 2) }

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  c-b-d
7.  a  \mneq{}  b
8.  b  \mneq{}  c
9.  b  \mneq{}  d
10.  a'  :  Point
11.  c'  :  Point
12.  z'  :  Point
13.  b\_a\_a'
14.  b\_c\_c'
15.  b\_d\_z'
16.  ba'  \mcong{}  ba'
17.  bc'  \mcong{}  bz'
18.  a'c'  \mcong{}  a'z'
\mvdash{}  Ra'bc'


By

---

Latex:
(D  0  THEN  Auto  THEN  (Assert  c'=b=z'  BY  (D  0  THEN  Auto))  THEN  GeometryFor  ``geo-midpoint  geo-eq``  2)

---

Home Index