for G being addGroup
for H1, H2 being Subgroup of G holds
( ( (carr H1) + (carr H2) = (carr H2) + (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) + (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) + (carr H2) implies (carr H1) + (carr H2) = (carr H2) + (carr H1) ) )