---

Step * 2 1 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_x'
19. b_d_z'
20. ba' ≅ bx'
21. bc' ≅ bz'
22. a'c' ≅ x'z'
⊢ Rabc
BY
{ ((InstLemma `geo-inner-three-segment` [⌜e⌝;⌜a'⌝;⌜a⌝;⌜b⌝;⌜x'⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN (FLemma `geo-construction-unicity` [-8;-6] THENA Auto)
   THEN (gEliminatePoint (-1) 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'
⊢ 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\_x'
19.  b\_d\_z'
20.  ba'  \mcong{}  bx'
21.  bc'  \mcong{}  bz'
22.  a'c'  \mcong{}  x'z'
\mvdash{}  Rabc


By

---

Latex:
((InstLemma  `geo-inner-three-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `geo-construction-unicity`  [-8;-6]  THENA  Auto)
  THEN  (gEliminatePoint  (-1)  THENA  Auto))

---

Home Index