---

Step * of Lemma es-interface-vals-singleton

∀[X,es,e:Top].  (X([e]) ~ [X(e)])
BY
{ (RepUR ``eclass-vals`` 0⋅ THEN Auto) }

---

Latex:


\mforall{}[X,es,e:Top].    (X([e])  \msim{}  [X(e)])


By

(RepUR  ``eclass-vals``  0\mcdot{}  THEN  Auto)

---

Home Index