---

Step * 1 of Lemma stable_point-eq

.....assertion..... 
1. e : EuclideanPlane
2. p : Point
3. q : Point
4. ¬¬(p = q ∈ Point)
⊢ pq=pp
BY
{ EuContradiction }

1
1. e : EuclideanPlane
2. p : Point
3. q : Point
4. ¬¬(p = q ∈ Point)
5. ¬pq=pp
⊢ False

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanPlane
2.  p  :  Point
3.  q  :  Point
4.  \mneg{}\mneg{}(p  =  q)
\mvdash{}  pq=pp


By

---

Latex:
EuContradiction

---

Home Index