---

Step * 1 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)
⊢ (¬(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'))
BY
{ D 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)

2
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. ¬(a = b ∈ Point)
6. ¬(c = 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{}  (\mneg{}(a  =  b))
\mwedge{}  (\mneg{}(c  =  b))
\mwedge{}  (\mneg{}(c  =  b))
\mwedge{}  (\mneg{}(a  =  b))
\mwedge{}  (\mexists{}a',c',x',z':Point.  (b\_a\_a'  \mwedge{}  b\_c\_c'  \mwedge{}  b\_c\_x'  \mwedge{}  b\_a\_z'  \mwedge{}  ba'=bx'  \mwedge{}  bc'=bz'  \mwedge{}  a'c'=x'z'))


By

---

Latex:
D  0

---

Home Index