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

for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds

H1 is StableSubgroup of H2

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds

H1 is StableSubgroup of H2

let H1, H2 be StableSubgroup of G; :: thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is StableSubgroup of H2 )

reconsider H19 = H1, H29 = H2 as Subgroup of G by Def7;

assume A1: the carrier of H1 c= the carrier of H2 ; :: thesis: H1 is StableSubgroup of H2

hence H1 is StableSubgroup of H2 by A2, Def7; :: thesis: verum

for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds

H1 is StableSubgroup of H2

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds

H1 is StableSubgroup of H2

let H1, H2 be StableSubgroup of G; :: thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is StableSubgroup of H2 )

reconsider H19 = H1, H29 = H2 as Subgroup of G by Def7;

assume A1: the carrier of H1 c= the carrier of H2 ; :: thesis: H1 is StableSubgroup of H2

A2: now :: thesis: for o being Element of O holds H1 ^ o = (H2 ^ o) | the carrier of H1

H19 is Subgroup of H29
by A1, GROUP_2:57;let o be Element of O; :: thesis: H1 ^ o = (H2 ^ o) | the carrier of H1

thus H1 ^ o = (G ^ o) | the carrier of H1 by Def7

.= ((G ^ o) | the carrier of H2) | the carrier of H1 by A1, RELAT_1:74

.= (H2 ^ o) | the carrier of H1 by Def7 ; :: thesis: verum

end;thus H1 ^ o = (G ^ o) | the carrier of H1 by Def7

.= ((G ^ o) | the carrier of H2) | the carrier of H1 by A1, RELAT_1:74

.= (H2 ^ o) | the carrier of H1 by Def7 ; :: thesis: verum

hence H1 is StableSubgroup of H2 by A2, Def7; :: thesis: verum