let H1, H2 be strict Subgroup of G; :: thesis: ( A c= the carrier of H1 & ( for H being strict Subgroup of G st A c= the carrier of H holds
H1 is Subgroup of H ) & A c= the carrier of H2 & ( for H being strict Subgroup of G st A c= the carrier of H holds
H2 is Subgroup of H ) implies H1 = H2 )
assume ( A c= the carrier of H1 & ( for H being strict Subgroup of G st A c= the carrier of H holds
H1 is Subgroup of H ) & A c= the carrier of H2 & ( for H being strict Subgroup of G st A c= the carrier of H holds
H2 is Subgroup of H ) ) ; :: thesis: H1 = H2
then ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) ;
hence H1 = H2 by GROUP_2:55; :: thesis: verum