set SS = { B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } ;
{ B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } c= bool X

proof

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

end;

hence { B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } is Subset-Family of X ; :: thesis: verum