for G being addGroup
for A being Subset of G st A <> {} holds
( ([#] the carrier of G) + A = the carrier of G & A + ([#] the carrier of G) = the carrier of G )