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