---

Step * of Lemma es-E-interface-conditional-subtype_rel

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y,Z:EClass(Top)].  (E([X?Y]) ⊆r E(Z)) supposing ((E(Y) ⊆r E(Z)) and (E(X) ⊆r E(Z)))
BY
{ Auto }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
5. Z : EClass(Top)
6. E(X) ⊆r E(Z)
7. E(Y) ⊆r E(Z)
⊢ E([X?Y]) ⊆r E(Z)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y,Z:EClass(Top)].
    (E([X?Y])  \msubseteq{}r  E(Z))  supposing  ((E(Y)  \msubseteq{}r  E(Z))  and  (E(X)  \msubseteq{}r  E(Z)))


By

Auto

---

Home Index