{ 
A:Id List. W:{a:Id| (a 
A)} List List.
(three-intersection(A;W) 
two-intersection(A;W)) }
{ Proof }
Definitions occuring in Statement :
three-intersection: three-intersection(A;W),
two-intersection: two-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,
two-intersection: two-intersection(A;W),
l_all: (xL.P[x]),
exists: 
x:A. B[x],
and: P 
Q,
member: t T,
prop: 
,
cand: A c B,
three-intersection: three-intersection(A;W)
Lemmas :
l_member_wf,
three-intersection_wf,
Id_wf
\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. (three-intersection(A;W) {}\mRightarrow{} two-intersection(A;W))
Date html generated:
2010_08_27-AM-12_50_11
Last ObjectModification:
2009_12_23-PM-03_26_36
Home
Index