---

Step * 1 1 of Lemma stable_point-eq


1. e : EuclideanPlane
2. p : Point
3. q : Point
4. ¬¬(p = q ∈ Point)
5. ¬pq=pp
⊢ False
BY
{ (D -2 THEN ParallelLast) }

1
1. e : EuclideanPlane
2. p : Point
3. q : Point
4. p = q ∈ Point
⊢ pq=pp

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -2  THEN  ParallelLast)

---

Home Index