let G be addGroup; :: thesis: for A being Subset of G st ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 + g2 in A ) & ( for g being Element of G st g in A holds
- g in A ) holds
A + A = A
let A be Subset of G; :: thesis: ( ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 + g2 in A ) & ( for g being Element of G st g in A holds
- g in A ) implies A + A = A )
assume that
A1: for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 + g2 in A and
A2: for g being Element of G st g in A holds
- g in A ; :: thesis: A + A = A
thus A + A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= A + A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + A or x in A )
assume x in A + A ; :: thesis: x in A
then ex g1, g2 being Element of G st
( x = g1 + g2 & g1 in A & g2 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 + A )
assume A3: x in A ; :: thesis: x in A + A
then reconsider a = x as Element of G ;
- a in A by A2, A3;
then (- a) + a in A by A1, A3;
then A4: 0_ G in A by Def5;
(0_ G) + a = a by Def4;
hence x in A + A by A3, A4; :: thesis: verum