---

{ A:Id List. W:{a:Id| (a  A)}  List List.
    (two-intersection(A;W)  one-intersection(A;W)) }

{ Proof }

---

Definitions occuring in Statement :  two-intersection: two-intersection(A;W),  one-intersection: one-intersection(A;W),  Id: Id,  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  list: type List,  l_member: (x  l)
Definitions :  all: x:A. B[x],  implies: P  Q,  one-intersection: one-intersection(A;W),  l_all: (xL.P[x]),  exists: x:A. B[x],  member: t  T,  two-intersection: two-intersection(A;W),  and: P  Q,  prop:
Lemmas :  l_member_wf,  two-intersection_wf,  Id_wf

---

\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.    (two-intersection(A;W)  {}\mRightarrow{}  one-intersection(A;W))


Date html generated: 2010_08_27-AM-12_50_13
Last ObjectModification: 2009_12_23-PM-03_26_39

Home Index