theorem Th22: :: GROUP_1A:68

for G being addGroup
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