let O be set ; :: thesis: for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G st ( for g being Element of G st g in H1 holds

g in H2 ) holds

H1 is StableSubgroup of H2

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st ( for g being Element of G st g in H1 holds

g in H2 ) holds

H1 is StableSubgroup of H2

let H1, H2 be StableSubgroup of G; :: thesis: ( ( for g being Element of G st g in H1 holds

g in H2 ) implies H1 is StableSubgroup of H2 )

assume A1: for g being Element of G st g in H1 holds

g in H2 ; :: thesis: H1 is StableSubgroup of H2

the carrier of H1 c= the carrier of H2

for H1, H2 being StableSubgroup of G st ( for g being Element of G st g in H1 holds

g in H2 ) holds

H1 is StableSubgroup of H2

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st ( for g being Element of G st g in H1 holds

g in H2 ) holds

H1 is StableSubgroup of H2

let H1, H2 be StableSubgroup of G; :: thesis: ( ( for g being Element of G st g in H1 holds

g in H2 ) implies H1 is StableSubgroup of H2 )

assume A1: for g being Element of G st g in H1 holds

g in H2 ; :: thesis: H1 is StableSubgroup of H2

the carrier of H1 c= the carrier of H2

proof

hence
H1 is StableSubgroup of H2
by Lm20; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of H1 or x in the carrier of H2 )

assume x in the carrier of H1 ; :: thesis: x in the carrier of H2

then reconsider g = x as Element of H1 ;

reconsider g = g as Element of G by Th2;

g in H1 by STRUCT_0:def 5;

then g in H2 by A1;

hence x in the carrier of H2 by STRUCT_0:def 5; :: thesis: verum

end;assume x in the carrier of H1 ; :: thesis: x in the carrier of H2

then reconsider g = x as Element of H1 ;

reconsider g = g as Element of G by Th2;

g in H1 by STRUCT_0:def 5;

then g in H2 by A1;

hence x in the carrier of H2 by STRUCT_0:def 5; :: thesis: verum