---

Step * of Lemma interface_predicate_set_lemma

∀X,es:Top.  ({e:E| {X} e}  ~ E(X))
BY
{ (UnivCD THENA Auto) }

1
1. X : Top@i
2. es : Top@i
⊢ {e:E| {X} e}  ~ E(X)

---

Latex:


\mforall{}X,es:Top.    (\{e:E|  \{X\}  e\}    \msim{}  E(X))


By

(UnivCD  THENA  Auto)

---

Home Index