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 " <> {} )

set x = the Element of A " ;

thus ( A <> {} implies A " <> {} ) :: thesis: ( A " <> {} implies A <> {} )

then ex a being Element of G st

( the Element of A " = a " & a in A ) by Th2;

hence A <> {} ; :: thesis: verum

( A <> {} iff A " <> {} )

let A be Subset of G; :: thesis: ( A <> {} iff A " <> {} )

set x = the Element of A " ;

thus ( A <> {} implies A " <> {} ) :: thesis: ( A " <> {} implies A <> {} )

proof

assume
A " <> {}
; :: thesis: A <> {}
set x = the Element of A;

assume A1: A <> {} ; :: thesis: A " <> {}

then reconsider x = the Element of A as Element of G by Lm1;

x " in A " by A1;

hence A " <> {} ; :: thesis: verum

end;assume A1: A <> {} ; :: thesis: A " <> {}

then reconsider x = the Element of A as Element of G by Lm1;

x " in A " by A1;

hence A " <> {} ; :: thesis: verum

then ex a being Element of G st

( the Element of A " = a " & a in A ) by Th2;

hence A <> {} ; :: thesis: verum