---

Step * of Lemma ss-mem-basic-whole

No Annotations
∀X:SeparationSpace. ∀x:Point(X).  uiff(x ∈ ss-basic-whole();True)
BY
{ (Auto
   THEN Unfolds ``ss-mem-basic ss-basic-whole`` 0
   THEN Unfold `l_all` 0
   THEN Reduce 0
   THEN Auto
   THEN IntSegCases (-1)
   THEN Reduce 0
   THEN RepUR ``ss-const ss-ap`` 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfolds  ``ss-mem-basic  ss-basic-whole``  0
  THEN  Unfold  `l\_all`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  IntSegCases  (-1)
  THEN  Reduce  0
  THEN  RepUR  ``ss-const  ss-ap``  0
  THEN  Auto)

---

Home Index