now

let x be set ; :: thesis: ( x in bool {} iff x in {{}} )
( x 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:1; :: thesis: verum