{ (S [~]) where S is Element of SF : verum } c= bool [:X,X:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (S [~]) where S is Element of SF : verum } or x in bool [:X,X:] )
assume x in { (S [~]) where S is Element of SF : verum } ; :: thesis: x in bool [:X,X:]
then ex S being Element of SF st x = S [~] ;
hence x in bool [:X,X:] ; :: thesis: verum
end;
hence { (S [~]) where S is Element of SF : verum } is Subset-Family of [:X,X:] ; :: thesis: verum