for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
the carrier of (H1 "\/" H2) = H1 * H2