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

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

let y be object ; :: thesis: ( y in bool {x} iff y in {{},{x}} )
reconsider yy = y as set by TARSKI:1;
( yy 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