---

Step * of Lemma stable_point-eq

∀[e:EuclideanPlane]. ∀[p,q:Point].  Stable{p = q ∈ Point}
BY
{ (Auto THEN (D 0 THENA Auto) THEN Assert ⌜pq=pp⌝⋅) }

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

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

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[p,q:Point].    Stable\{p  =  q\}


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  Assert  \mkleeneopen{}pq=pp\mkleeneclose{}\mcdot{})

---

Home Index