set S = singletons X;
singletons X c= bool X

proof

let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in singletons X or f in bool X )
assume f in singletons X ; :: thesis: f in bool X
then ex g being Subset of X st
( f = g & g is Singleton ) ;
then reconsider f = f as Subset of X ;
f is Element of bool X ;
hence f in bool X ; :: thesis: verum

end;

hence singletons X is Subset of (bspace X) ; :: thesis: verum