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 that
A25: A c= the carrier of H1 and
A26: ( ( 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 ) and
A27: for H being strict StableSubgroup of G st A c= the carrier of H holds
H2 is StableSubgroup of H ; :: thesis: H1 = H2
H1 is StableSubgroup of H2 by A26;
then H1 is Subgroup of H2 by Def7;
then A28: the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
H2 is StableSubgroup of H1 by A25, A27;
then H2 is Subgroup of H1 by Def7;
then the carrier of H2 c= the carrier of H1 by GROUP_2:def 5;
then the carrier of H1 = the carrier of H2 by A28, XBOOLE_0:def 10;
hence H1 = H2 by Lm5; :: thesis: verum