let G be addGroup; :: 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 <> {} )

proof

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 - A <> {} ; :: thesis: A <> {}
then ex a being Element of G st
( the Element of - A = - a & a in A ) by Th2;
hence A <> {} ; :: thesis: verum