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
A23: A c= the carrier of H1 and
A24: ( ( 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
A25: 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 A24;
then H1 is Subgroup of H2 by Def7;
then A26: the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
H2 is StableSubgroup of H1 by A23, A25;
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 A26, XBOOLE_0:def 10;
hence H1 = H2 by Lm4; :: thesis: verum