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 object such that
A2: y in {_{X}_} by XBOOLE_0:def 1;
ex x being object st
( y = {x} & x in X ) by A2, Th1;
hence contradiction by A1; :: thesis: verum
end;
assume A3: {_{X}_} = {} ; :: thesis: X = {}
assume not X = {} ; :: thesis: contradiction
then consider x being object such that
A4: x in X by XBOOLE_0:def 1;
{x} in {_{X}_} by A4, Th1;
hence contradiction by A3; :: thesis: verum