let X be set ; :: thesis: ( X = {} iff {_{X}_} = {} )
thus ( X = {} implies {_{X}_} = {} ) :: thesis: ( {_{X}_} = {} implies X = {} )

proof

assume A1: X = {} ; :: thesis: {_{X}_} = {}
assume not {_{X}_} = {} ; :: thesis: contradiction
then consider y being set such that
A2: y in {_{X}_} by XBOOLE_0:def 1;
consider x being set such that
A3: ( y = {x} & x in X ) by A2, Th1;
thus contradiction by A1, A3; :: thesis: verum

end;

assume A4: {_{X}_} = {} ; :: thesis: X = {}
assume not X = {} ; :: thesis: contradiction
then consider x being set such that
A5: x in X by XBOOLE_0:def 1;
{x} in {_{X}_} by A5, Th1;
hence contradiction by A4; :: thesis: verum