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