let G be Group; :: thesis: for g1, g2 being Element of G

for H being Subgroup of G st g1 in H & g2 in H holds

g1 * g2 in H

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

g1 * g2 in H

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

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

then reconsider h1 = g1, h2 = g2 as Element of H ;

h1 * h2 in H ;

hence g1 * g2 in H by Th43; :: thesis: verum

for H being Subgroup of G st g1 in H & g2 in H holds

g1 * g2 in H

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

g1 * g2 in H

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

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

then reconsider h1 = g1, h2 = g2 as Element of H ;

h1 * h2 in H ;

hence g1 * g2 in H by Th43; :: thesis: verum