theorem Th22: :: GROUP_2:22

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