---

Step * 2 1 1 1 1 of Lemma adjacent-right-angles-supplementary

.....assertion..... 
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. u : Point
26. u=b=c'
⊢ u ≡ z'
BY
{ ((Assert c'_b_z' BY
          Auto)
   THEN ((Assert c'=b=z' BY Unfold `geo-midpoint` 0) THEN Auto)
   THEN InstLemma `symmetric-point-unicity` [⌜e⌝;⌜b⌝;⌜c'⌝;⌜u⌝;⌜z'⌝]⋅
   THEN EAuto 1) }

---

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.  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.  u  :  Point
26.  u=b=c'
\mvdash{}  u  \mequiv{}  z'


By

---

Latex:
((Assert  c'\_b\_z'  BY
                Auto)
  THEN  ((Assert  c'=b=z'  BY  Unfold  `geo-midpoint`  0)  THEN  Auto)
  THEN  InstLemma  `symmetric-point-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index