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

for H being StableSubgroup of G

for g being Element of G st g in H holds

g " in H

let G be GroupWithOperators of O; :: thesis: for H being StableSubgroup of G

for g being Element of G st g in H holds

g " in H

let H be StableSubgroup of G; :: thesis: for g being Element of G st g in H holds

g " in H

let g be Element of G; :: thesis: ( g in H implies g " in H )

assume A1: g in H ; :: thesis: g " in H

H is Subgroup of G by Def7;

hence g " in H by A1, GROUP_2:51; :: thesis: verum

for H being StableSubgroup of G

for g being Element of G st g in H holds

g " in H

let G be GroupWithOperators of O; :: thesis: for H being StableSubgroup of G

for g being Element of G st g in H holds

g " in H

let H be StableSubgroup of G; :: thesis: for g being Element of G st g in H holds

g " in H

let g be Element of G; :: thesis: ( g in H implies g " in H )

assume A1: g in H ; :: thesis: g " in H

H is Subgroup of G by Def7;

hence g " in H by A1, GROUP_2:51; :: thesis: verum