---

Step * of Lemma es-E-interfaces-strong-subtype

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)].  uiff(E(X) ⊆r E(Y);strong-subtype(E(X);E(Y)))
BY
{ ((UnivCD THENA Auto) THEN D 0 THEN (D 0 THENA Auto)) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
5. E(X) ⊆r E(Y)
⊢ strong-subtype(E(X);E(Y))

2
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
5. strong-subtype(E(X);E(Y))
⊢ E(X) ⊆r E(Y)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].    uiff(E(X)  \msubseteq{}r  E(Y);strong-subtype(E(X);E(Y)))


By

((UnivCD  THENA  Auto)  THEN  D  0  THEN  (D  0  THENA  Auto))

---

Home Index