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

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

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;

H19 is Subgroup of H29 by A1, GROUP_2:57;
hence H1 is StableSubgroup of H2 by A2, Def7; :: thesis: verum