set FIC = subset-closed_closure_of F;
subset-closed_closure_of F c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in subset-closed_closure_of F or x in bool X )
reconsider xx = x as set by TARSKI:1;
assume x in subset-closed_closure_of F ; :: thesis: x in bool X
then ex y being set st
( xx c= y & y in F ) by Th2;
then xx c= X by XBOOLE_1:1;
hence x in bool X ; :: thesis: verum

end;

hence subset-closed_closure_of F is subset-closed Subset-Family of X ; :: thesis: verum