---

Step * of Lemma ss-mem-empty

No Annotations
∀[X:SeparationSpace]. ∀[x:Point(X)].  uiff(x ∈ ss-empty();False)
BY
{ (((Intros THEN RepUR ``ss-mem-open ss-empty`` 0) THEN Auto) THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:SeparationSpace].  \mforall{}[x:Point(X)].    uiff(x  \mmember{}  ss-empty();False)


By

---

Latex:
(((Intros  THEN  RepUR  ``ss-mem-open  ss-empty``  0)  THEN  Auto)  THEN  ExRepD  THEN  Auto)

---

Home Index