let G be addGroup; :: thesis: for H1, H2 being Subgroup of G st G is Abelian addGroup 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 Abelian addGroup implies ex H being strict Subgroup of G st the carrier of H = (carr H1) + (carr H2) )
assume G is Abelian addGroup ; :: 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