---

Step * 1 1 1 of Lemma stable_point-eq


1. e : EuclideanPlane
2. p : Point
3. q : Point
4. p = q ∈ Point
⊢ pq=pp
BY
{ (HypSubst' (-1) 0 THEN Auto) }

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

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Point
3.  q  :  Point
4.  p  =  q
\mvdash{}  pq=pp


By

---

Latex:
(HypSubst'  (-1)  0  THEN  Auto)

---

Home Index