---

Step * 2 1 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. 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
BY
{ (Assert ⌜Ra'bc'⌝⋅ THENM GeometryFor ``right-angle geo-colinear geo-sep`` 2) }

1
.....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'

---

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.  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{}  Rabc


By

---

Latex:
(Assert  \mkleeneopen{}Ra'bc'\mkleeneclose{}\mcdot{}  THENM  GeometryFor  ``right-angle  geo-colinear  geo-sep``  2)

---

Home Index