---

Step * of Lemma es-E-interface-predicate

∀[es,B,I:Top].  ({e:E| {I} e}  ~ E(I))
BY
{ (RepUR ``es-interface-predicate es-E-interface`` 0 THEN Auto) }

---

Latex:


\mforall{}[es,B,I:Top].    (\{e:E|  \{I\}  e\}    \msim{}  E(I))


By

(RepUR  ``es-interface-predicate  es-E-interface``  0  THEN  Auto)

---

Home Index