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

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