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