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:
Latex:
\mforall{}X,es:Top.    (\{e:E|  \{X\}  e\}    \msim{}  E(X))
By
Latex:
(UnivCD  THENA  Auto)
Home
Index