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

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