---

Step * 2 1 1 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. 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
BY
{ ((Assert Colinear(b;a';a) BY Auto) THEN (FLemma `right-angle-colinear` [-1;-2] THENA Auto)) }

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_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'
26. Colinear(b;a';a)
27. Rabc'
⊢ 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'
25.  Ra'bc'
\mvdash{}  Rabc


By

---

Latex:
((Assert  Colinear(b;a';a)  BY  Auto)  THEN  (FLemma  `right-angle-colinear`  [-1;-2]  THENA  Auto))

---

Home Index