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 A1: ( a in H & b in H ) ; :: thesis: [.a,b.] in H
then ( a " in H & b " in H ) by GROUP_2:51;
then A2: (a ") * (b ") in H by GROUP_2:50;
a * b in H by A1, GROUP_2:50;
then ((a ") * (b ")) * (a * b) in H by A2, GROUP_2:50;
hence [.a,b.] in H by Th16; :: thesis: verum