let G be Group; :: thesis: for H1, H2 being Subgroup of G st G is commutative Group holds

ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)

let H1, H2 be Subgroup of G; :: thesis: ( G is commutative Group implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) )

assume G is commutative Group ; :: thesis: ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)

then (carr H1) * (carr H2) = (carr H2) * (carr H1) by Th25;

hence ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by Th78; :: thesis: verum

ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)

let H1, H2 be Subgroup of G; :: thesis: ( G is commutative Group implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) )

assume G is commutative Group ; :: thesis: ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)

then (carr H1) * (carr H2) = (carr H2) * (carr H1) by Th25;

hence ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by Th78; :: thesis: verum