---

Step * 1 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. (¬(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
BY
{ Unfold `eu-cong-angle` 0 }

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
⊢ (¬(a = b ∈ Point))
∧ (¬(c = b ∈ Point))
∧ (¬(x = y ∈ Point))
∧ (¬(z = y ∈ Point))
∧ (∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ y_x_x' ∧ y_z_z' ∧ ba'=yx' ∧ bc'=yz' ∧ a'c'=x'z'))

---

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.  (\mneg{}(x  =  y))
\mwedge{}  (\mneg{}(z  =  y))
\mwedge{}  (\mneg{}(a  =  b))
\mwedge{}  (\mneg{}(c  =  b))
\mwedge{}  (\mexists{}a',c',x',z':Point.  (y\_x\_a'  \mwedge{}  y\_z\_c'  \mwedge{}  b\_a\_x'  \mwedge{}  b\_c\_z'  \mwedge{}  ya'=bx'  \mwedge{}  yc'=bz'  \mwedge{}  a'c'=x'z'))@i
\mvdash{}  abc  =  xyz


By

---

Latex:
Unfold  `eu-cong-angle`  0

---

Home Index