---

Step * 1 of Lemma eu-cong-angle-symm2


1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. x : Point@i
6. y : Point@i
7. z : Point@i
8. xyz = abc@i
⊢ abc = xyz
BY
{ Unfold `eu-cong-angle` 8 }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. x : Point@i
6. y : Point@i
7. z : Point@i
8. (¬(x = y ∈ Point))
∧ (¬(z = y ∈ Point))
∧ (¬(a = b ∈ Point))
∧ (¬(c = b ∈ Point))
∧ (∃a',c',x',z':Point. (y_x_a' ∧ y_z_c' ∧ b_a_x' ∧ b_c_z' ∧ ya'=bx' ∧ yc'=bz' ∧ a'c'=x'z'))@i
⊢ abc = xyz

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  a  :  Point@i
3.  b  :  Point@i
4.  c  :  Point@i
5.  x  :  Point@i
6.  y  :  Point@i
7.  z  :  Point@i
8.  xyz  =  abc@i
\mvdash{}  abc  =  xyz


By

---

Latex:
Unfold  `eu-cong-angle`  8

---

Home Index