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