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 A1: f in singletons X ; :: thesis: f in bool X
consider g being Subset of X such that
A2: f = g and
g is Singleton by A1;
reconsider f = f as Subset of X by A2;
f is Element of bool X ;
hence f in bool X ; :: thesis: verum

end;

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