---

Step * of Lemma es-E-interface_functionality-iff

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)].  uiff(E(X) ⊆r E(Y);{∀[e:E]. ↑e ∈b Y supposing ↑e ∈b X})
BY
{ (Unfold `guard` 0 THEN (Unfold `es-E-interface` 0 THEN Auto)⋅) }

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

---

Latex:


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


By

(Unfold  `guard`  0  THEN  (Unfold  `es-E-interface`  0  THEN  Auto)\mcdot{})

---

Home Index