theorem :: GROUP_3:56

for G being Group holds
( G is commutative Group iff for A being Subset of G
for g being Element of G holds A |^ g = A )