---

Step * 1 1 2 2 2 2 1 of Lemma eu-cong-angle-symm


1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. ¬(a = b ∈ Point)
6. ¬(c = b ∈ Point)
7. x : Point
8. b_a_x
9. ax=bc
10. y : Point
11. b_c_y
12. cy=ba
13. b_a_x
14. b_c_y
15. b_c_y
16. b_a_x
⊢ bx=by
BY
{ (InstLemma `eu-three-segment` [⌜e⌝;⌜b⌝;⌜a⌝;⌜x⌝;⌜y⌝;⌜c⌝;⌜b⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  a  :  Point@i
3.  b  :  Point@i
4.  c  :  Point@i
5.  \mneg{}(a  =  b)
6.  \mneg{}(c  =  b)
7.  x  :  Point
8.  b\_a\_x
9.  ax=bc
10.  y  :  Point
11.  b\_c\_y
12.  cy=ba
13.  b\_a\_x
14.  b\_c\_y
15.  b\_c\_y
16.  b\_a\_x
\mvdash{}  bx=by


By

---

Latex:
(InstLemma  `eu-three-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index