---

Step * of Lemma ss-const_wf

∀[X,Y:SeparationSpace]. ∀[c:Point(Y)].  (ss-const(c) ∈ Point(X ⟶ Y))
BY
{ (Auto
   THEN (RWO "ss-fun-point" 0 THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``ss-const ss-function`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,Y:SeparationSpace].  \mforall{}[c:Point(Y)].    (ss-const(c)  \mmember{}  Point(X  {}\mrightarrow{}  Y))


By

---

Latex:
(Auto
  THEN  (RWO  "ss-fun-point"  0  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``ss-const  ss-function``  0
  THEN  Auto)

---

Home Index