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