---

{ [Info,A,B,C:Type]. [X:EClass(A)]. [Y:EClass(B)]. [Z:EClass(C)].
    ((X,Y,Z)  EClass(A  B  C)) }

{ Proof }

---

Definitions occuring in Statement :  es-interface-triple: (X,Y,Z),  eclass: EClass(A[eo; e]),  uall: [x:A]. B[x],  member: t  T,  product: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  es-interface-triple: (X,Y,Z),  so_lambda: x y.t[x; y],  so_apply: x[s1;s2],  all: x:A. B[x],  subtype: S  T
Lemmas :  es-interface-pair_wf,  eclass_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf

---

\mforall{}[Info,A,B,C:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(C)].    ((X,Y,Z)  \mmember{}  EClass(A  \mtimes{}  B  \mtimes{}  C))


Date html generated: 2011_08_16-PM-05_37_57
Last ObjectModification: 2011_06_20-AM-01_28_41

Home Index