now :: thesis: for x being object holds
( x in bool {} iff x in {{}} )

let x be object ; :: thesis: ( x in bool {} iff x in {{}} )
reconsider xx = x as set by TARSKI:1;
( xx c= {} iff x = {} ) by XBOOLE_1:3;
hence ( x in bool {} iff x in {{}} ) by Def1, TARSKI:def 1; :: thesis: verum

end;

hence bool {} = {{}} by TARSKI:2; :: thesis: verum