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