---

Step * 1 1 1 of Lemma interface_predicate_set_lemma


1. X : Top@i
2. es : Top@i
⊢ {e:E| ↑e ∈b X}  ~ {e:E| ↑e ∈b X} 
BY
{ Try SqEqCD }

---

Latex:



1.  X  :  Top@i
2.  es  :  Top@i
\mvdash{}  \{e:E|  \muparrow{}e  \mmember{}\msubb{}  X\}    \msim{}  \{e:E|  \muparrow{}e  \mmember{}\msubb{}  X\} 


By

Try  SqEqCD

---

Home Index