let G be Group; :: thesis: for g1, g2 being Element of G
for H being Subgroup of G st g1 in carr H & g2 in carr H holds
g1 * g2 in carr H
let g1, g2 be Element of G; :: thesis: for H being Subgroup of G st g1 in carr H & g2 in carr H holds
g1 * g2 in carr H
let H be Subgroup of G; :: thesis: ( g1 in carr H & g2 in carr H implies g1 * g2 in carr H )
assume ( g1 in carr H & g2 in carr H ) ; :: thesis: g1 * g2 in carr H
then ( g1 in H & g2 in H ) by STRUCT_0:def 5;
then g1 * g2 in H by Th59;
hence g1 * g2 in carr H by STRUCT_0:def 5; :: thesis: verum