let G be Group; :: thesis: for A being Subset of G holds
( A <> {} iff A " <> {} )
let A be Subset of G; :: thesis: ( A <> {} iff A " <> {} )
consider x being Element of A " ;
thus ( A <> {} implies A " <> {} ) :: thesis: ( A " <> {} implies A <> {} )

proof

consider x being Element of A;
assume A1: A <> {} ; :: thesis: A " <> {}
then reconsider x = x as Element of G by Lm1;
x " in A " by A1;
hence A " <> {} ; :: thesis: verum

end;

assume A " <> {} ; :: thesis: A <> {}
then ex a being Element of G st
( x = a " & a in A ) by Th5;
hence A <> {} ; :: thesis: verum