set B = { A where A is Subset of X : [A,X] in Maximal_wrt F } ;
{ A where A is Subset of X : [A,X] in Maximal_wrt F } c= bool X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of X : [A,X] in Maximal_wrt F } or x in bool X )
assume x in { A where A is Subset of X : [A,X] in Maximal_wrt F } ; :: thesis: x in bool X
then ex A being Subset of X st
( x = A & [A,X] in Maximal_wrt F ) ;
hence x in bool X ; :: thesis: verum

end;

hence { A where A is Subset of X : [A,X] in Maximal_wrt F } is Subset-Family of X ; :: thesis: verum