set B = { b where b is Subset of X : for x, y being Subset of X st [x,y] in F & x c= b holds
y c= b } ;
{ b where b is Subset of X : for x, y being Subset of X st [x,y] in F & x c= b holds
y c= b } c= bool X

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { b where b is Subset of X : for x, y being Subset of X st [x,y] in F & x c= b holds
y c= b } or z in bool X )
assume z in { b where b is Subset of X : for x, y being Subset of X st [x,y] in F & x c= b holds
y c= b } ; :: thesis: z in bool X
then ex b being Subset of X st
( z = b & ( for x, y being Subset of X st [x,y] in F & x c= b holds
y c= b ) ) ;
hence z in bool X ; :: thesis: verum

end;

hence { b where b is Subset of X : for A, B being Subset of X st [A,B] in F & A c= b holds
B c= b } is Subset-Family of X ; :: thesis: verum