let G be addGroup; :: thesis: for A being Subset of G st ( for g being Element of G st g in A holds
- g in A ) holds
- A = A
let A be Subset of G; :: thesis: ( ( for g being Element of G st g in A holds
- g in A ) implies - A = A )
assume A1: for g being Element of G st g in A holds
- g in A ; :: thesis: - A = A
thus - A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= - A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in - A or x in A )
assume x in - A ; :: thesis: x in A
then ex g being Element of G st
( x = - g & g in A ) ;
hence x in A by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in - A )
assume A2: x in A ; :: thesis: x in - A
then reconsider a = x as Element of G ;
A3: x = - (- a) ;
- a in A by A1, A2;
hence x in - A by A3; :: thesis: verum