let G be Group; :: thesis: for a, b being Element of G

for H being Subgroup of G st a in H & b in H holds

a |^ b in H

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

a |^ b in H

let H be Subgroup of G; :: thesis: ( a in H & b in H implies a |^ b in H )

assume ( a in H & b in H ) ; :: thesis: a |^ b in H

then ( b " in H & a * b in H ) by GROUP_2:50, GROUP_2:51;

then (b ") * (a * b) in H by GROUP_2:50;

hence a |^ b in H by GROUP_1:def 3; :: thesis: verum

for H being Subgroup of G st a in H & b in H holds

a |^ b in H

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

a |^ b in H

let H be Subgroup of G; :: thesis: ( a in H & b in H implies a |^ b in H )

assume ( a in H & b in H ) ; :: thesis: a |^ b in H

then ( b " in H & a * b in H ) by GROUP_2:50, GROUP_2:51;

then (b ") * (a * b) in H by GROUP_2:50;

hence a |^ b in H by GROUP_1:def 3; :: thesis: verum