---

{ [Info,T:Type]. [X:EClass(T)]. [L:bag(Id)].
    (class-loc-bound{i:l}(Info;T;X;L)  ') }

{ Proof }

---

Definitions occuring in Statement :  class-loc-bound: class-loc-bound{i:l}(Info;T;X;L),  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  prop: ,  member: t  T,  universe: Type,  bag: bag(T)
Lemmas :  es-loc_wf,  bag-member_wf,  Id_wf,  classrel_wf,  event-ordering+_inc,  es-E_wf,  event-ordering+_wf,  eclass_wf,  bag_wf

---

\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[L:bag(Id)].    (class-loc-bound\{i:l\}(Info;T;X;L)  \mmember{}  \mBbbP{}')


Date html generated: 2011_08_16-AM-11_29_54
Last ObjectModification: 2011_06_30-PM-12_19_45

Home Index