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

for H being StableSubgroup of G

for g1, g2 being Element of G st g1 in H & g2 in H holds

g1 * g2 in H

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

for g1, g2 being Element of G st g1 in H & g2 in H holds

g1 * g2 in H

let H be StableSubgroup of G; :: thesis: for g1, g2 being Element of G st g1 in H & g2 in H holds

g1 * g2 in H

let g1, g2 be Element of G; :: thesis: ( g1 in H & g2 in H implies g1 * g2 in H )

assume A1: ( g1 in H & g2 in H ) ; :: thesis: g1 * g2 in H

H is Subgroup of G by Def7;

hence g1 * g2 in H by A1, GROUP_2:50; :: thesis: verum

for H being StableSubgroup of G

for g1, g2 being Element of G st g1 in H & g2 in H holds

g1 * g2 in H

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

for g1, g2 being Element of G st g1 in H & g2 in H holds

g1 * g2 in H

let H be StableSubgroup of G; :: thesis: for g1, g2 being Element of G st g1 in H & g2 in H holds

g1 * g2 in H

let g1, g2 be Element of G; :: thesis: ( g1 in H & g2 in H implies g1 * g2 in H )

assume A1: ( g1 in H & g2 in H ) ; :: thesis: g1 * g2 in H

H is Subgroup of G by Def7;

hence g1 * g2 in H by A1, GROUP_2:50; :: thesis: verum