---

Step * 1 1 1 1 2 1 of Lemma angle-bisector-unique


1. e : EuclideanPlane
2. z : Point
3. a : Point
4. b : Point
5. c : Point
6. a' : Point
7. c' : Point
8. x : Point
9. y : Point
10. a # bc
11. out(b aa')
12. out(b cc')
13. a-x-c
14. a'-y-c'
15. abx ≅a cbx
16. a'by ≅a c'by
17. x' : Point
18. a-x'-c
19. out(b yx')
20. a'by ≅a abx'
21. c'by ≅a cbx'
22. C : Point
23. c-b-C
24. bC ≅ OX
25. c'' : Point
26. C-b-c''
27. bc'' ≅ ba
28. out(b cc'')
29. cbx' ≅a c''bz
30. abx' ≅a abz
31. out(b x'z)
32. a-z-c''
33. z' : Point
34. cbx ≅a c''bz
35. abx ≅a abz
36. out(b xz)
37. a-z-c''
38. a=z=c''
39. a=z=c''
40. z' ≡ z
41. out(b xy)
⊢ abx ≅a a'by
BY
{ (InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜b⌝;⌜a⌝;⌜x⌝;⌜a'⌝;⌜y⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  z  :  Point
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  a'  :  Point
7.  c'  :  Point
8.  x  :  Point
9.  y  :  Point
10.  a  \#  bc
11.  out(b  aa')
12.  out(b  cc')
13.  a-x-c
14.  a'-y-c'
15.  abx  \mcong{}\msuba{}  cbx
16.  a'by  \mcong{}\msuba{}  c'by
17.  x'  :  Point
18.  a-x'-c
19.  out(b  yx')
20.  a'by  \mcong{}\msuba{}  abx'
21.  c'by  \mcong{}\msuba{}  cbx'
22.  C  :  Point
23.  c-b-C
24.  bC  \mcong{}  OX
25.  c''  :  Point
26.  C-b-c''
27.  bc''  \mcong{}  ba
28.  out(b  cc'')
29.  cbx'  \mcong{}\msuba{}  c''bz
30.  abx'  \mcong{}\msuba{}  abz
31.  out(b  x'z)
32.  a-z-c''
33.  z'  :  Point
34.  cbx  \mcong{}\msuba{}  c''bz
35.  abx  \mcong{}\msuba{}  abz
36.  out(b  xz)
37.  a-z-c''
38.  a=z=c''
39.  a=z=c''
40.  z'  \mequiv{}  z
41.  out(b  xy)
\mvdash{}  abx  \mcong{}\msuba{}  a'by


By

---

Latex:
(InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index