---

Step * of Lemma es-interface-subtype_rel2

∀[Info:Type]. ∀[A,B:es:EO+(Info) ─→ E ─→ Type].
  EClass(A[es;e]) ⊆r EClass(B[es;e]) supposing ∀es:EO+(Info). ∀e:E.  (A[es;e] ⊆r B[es;e])
BY
{ Auto }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[A,B:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type].
    EClass(A[es;e])  \msubseteq{}r  EClass(B[es;e])  supposing  \mforall{}es:EO+(Info).  \mforall{}e:E.    (A[es;e]  \msubseteq{}r  B[es;e])


By

Auto

---

Home Index