---

Step * 1 1 1 1 1 1 1 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)@i
9. ¬(z = y ∈ Point)@i
10. ¬(a = b ∈ Point)@i
11. ¬(c = b ∈ Point)@i
12. a' : Point@i
13. c' : Point@i
14. ∃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'))
BY
{ D 14 }

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)@i
9. ¬(z = y ∈ Point)@i
10. ¬(a = b ∈ Point)@i
11. ¬(c = b ∈ Point)@i
12. a' : Point@i
13. c' : Point@i
14. x' : Point@i
15. ∃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)@i
9.  \mneg{}(z  =  y)@i
10.  \mneg{}(a  =  b)@i
11.  \mneg{}(c  =  b)@i
12.  a'  :  Point@i
13.  c'  :  Point@i
14.  \mexists{}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{}  (\mneg{}(a  =  b))
\mwedge{}  (\mneg{}(c  =  b))
\mwedge{}  (\mneg{}(x  =  y))
\mwedge{}  (\mneg{}(z  =  y))
\mwedge{}  (\mexists{}a',c',x',z':Point.  (b\_a\_a'  \mwedge{}  b\_c\_c'  \mwedge{}  y\_x\_x'  \mwedge{}  y\_z\_z'  \mwedge{}  ba'=yx'  \mwedge{}  bc'=yz'  \mwedge{}  a'c'=x'z'))


By

---

Latex:
D  14

---

Home Index