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 " <> {} )
thus ( A <> {} implies A " <> {} ) :: thesis: ( A " <> {} implies A <> {} )

proof

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

end;

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