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 ( a " in H & b " in H & a * b in H ) by GROUP_2:59, GROUP_2:60;
then ( (a " ) * (b " ) in H & a * b in H ) by GROUP_2:59;
then ((a " ) * (b " )) * (a * b) in H by GROUP_2:59;
hence [.a,b.] in H by Th19; :: thesis: verum