---

Step * of Lemma ss-mem-whole

No Annotations
∀X:SeparationSpace. ∀x:Point(X).  uiff(x ∈ ss-whole(X);True)
BY
{ (((Intros THEN RepUR ``ss-mem-open ss-whole`` 0) THEN Auto)
   THEN D 0 With ⌜ss-basic-whole()⌝ 
   THEN Auto
   THEN BLemma `ss-mem-basic-whole`
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:SeparationSpace.  \mforall{}x:Point(X).    uiff(x  \mmember{}  ss-whole(X);True)


By

---

Latex:
(((Intros  THEN  RepUR  ``ss-mem-open  ss-whole``  0)  THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}ss-basic-whole()\mkleeneclose{} 
  THEN  Auto
  THEN  BLemma  `ss-mem-basic-whole`
  THEN  Auto)

---

Home Index