let G be Group; :: thesis: for H1, H2 being Subgroup of G st G is commutative Group holds
the carrier of (H1 "\/" H2) = H1 * H2
let H1, H2 be Subgroup of G; :: thesis: ( G is commutative Group implies the carrier of (H1 "\/" H2) = H1 * H2 )
assume G is commutative Group ; :: thesis: the carrier of (H1 "\/" H2) = H1 * H2
then H1 * H2 = H2 * H1 by GROUP_2:25;
hence the carrier of (H1 "\/" H2) = H1 * H2 by Th51; :: thesis: verum