for G being addGroup holds
( G is Abelian addGroup iff for A being Subset of G
for g being Element of G st A <> {} holds
g * A = {g} )