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:2; :: thesis: verum