set S = singletons X;

singletons X c= bool X

singletons X c= bool X

proof

hence
singletons X is Subset of (bspace X)
; :: thesis: verum
let f be object ; :: 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 1 -element ) ;

then reconsider f = f as Subset of X ;

f is Element of bool X ;

hence f in bool X ; :: thesis: verum

end;assume f in singletons X ; :: thesis: f in bool X

then ex g being Subset of X st

( f = g & g is 1 -element ) ;

then reconsider f = f as Subset of X ;

f is Element of bool X ;

hence f in bool X ; :: thesis: verum