Step
*
of Lemma
interface-part-subtype
∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[g:∩es:EO+(Info). (E(X) ─→ Id)]. ∀[i:Id]. ∀[es:EO+(Info)]. (E((X|g=i)) ⊆r E(X))
BY
{ (Auto THEN D 0 THEN Auto THEN DVar `x' THEN RWO "is-interface-part" (-1) THEN Auto) }
Latex:
Latex:
\mforall{}[Info,T:Type]. \mforall{}[X:EClass(T)]. \mforall{}[g:\mcap{}es:EO+(Info). (E(X) {}\mrightarrow{} Id)]. \mforall{}[i:Id]. \mforall{}[es:EO+(Info)].
(E((X|g=i)) \msubseteq{}r E(X))
By
Latex:
(Auto THEN D 0 THEN Auto THEN DVar `x' THEN RWO "is-interface-part" (-1) THEN Auto)
Home
Index