---

Step * of Lemma es-E-interface-conditional2

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)].  (E([X?Y]) ⊆r {e:E| (↑e ∈b Y) ∨ (↑e ∈b X)} )
BY
{ Auto }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
⊢ E([X?Y]) ⊆r {e:E| (↑e ∈b Y) ∨ (↑e ∈b X)} 

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].    (E([X?Y])  \msubseteq{}r  \{e:E|  (\muparrow{}e  \mmember{}\msubb{}  Y)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  X)\}  )


By

Auto

---

Home Index