---

{ S1,S2:Sys.  S1  S2 supposing S1 = S2 }

{ Proof }

---

Definitions occuring in Statement :  subsys: S1  S2,  Sys: Sys,  uimplies: b supposing a,  all: x:A. B[x],  equal: s = t
Definitions :  all: x:A. B[x],  uimplies: b supposing a,  subsys: S1  S2,  member: t  T,  so_lambda: x.t[x],  prop: ,  uall: [x:A]. B[x],  so_apply: x[s],  Sys: Sys
Lemmas :  sub-system_weakening,  name_wf,  mData_wf,  Sys_wf

---

\mforall{}S1,S2:Sys.    S1  \msubseteq{}  S2  supposing  S1  =  S2


Date html generated: 2011_08_17-PM-04_13_25
Last ObjectModification: 2011_06_18-AM-11_31_38

Home Index