---

Step * of Lemma ss-id_wf

∀[X:SeparationSpace]. (ss-id() ∈ Point(X ⟶ X))
BY
{ (Auto THEN (RWO "ss-fun-point" 0 THENA Auto) THEN MemTypeCD THEN Auto) }

1
1. X : SeparationSpace
⊢ ss-id() ∈ Point(X) ⟶ Point(X)

2
.....set predicate..... 
1. X : SeparationSpace
⊢ ss-function(X;X;ss-id())

---

Latex:

---

Latex:
\mforall{}[X:SeparationSpace].  (ss-id()  \mmember{}  Point(X  {}\mrightarrow{}  X))


By

---

Latex:
(Auto  THEN  (RWO  "ss-fun-point"  0  THENA  Auto)  THEN  MemTypeCD  THEN  Auto)

---

Home Index