---

Step * 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)
⊢ abc = cba
BY
{ Unfold `eu-cong-angle` 0 }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. ¬(a = b ∈ Point)
6. ¬(c = b ∈ Point)
⊢ (¬(a = b ∈ Point))
∧ (¬(c = b ∈ Point))
∧ (¬(c = b ∈ Point))
∧ (¬(a = b ∈ Point))
∧ (∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ b_c_x' ∧ b_a_z' ∧ ba'=bx' ∧ bc'=bz' ∧ a'c'=x'z'))

---

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)
\mvdash{}  abc  =  cba


By

---

Latex:
Unfold  `eu-cong-angle`  0

---

Home Index