let x be set ; :: thesis: bool {x} = {{} ,{x}}

now

let y be set ; :: thesis: ( y in bool {x} iff y in {{} ,{x}} )
( y c= {x} iff ( y = {} or y = {x} ) ) by Lm3;
hence ( y in bool {x} iff y in {{} ,{x}} ) by Def1, TARSKI:def 2; :: thesis: verum

end;

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