let G be Group; :: thesis: for H being Subgroup of G
for N being strict normal Subgroup of G holds
( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
let H be Subgroup of G; :: thesis: for N being strict normal Subgroup of G holds
( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
let N be strict normal Subgroup of G; :: thesis: ( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
thus commutators (H,N) c= carr N :: thesis: commutators (N,H) c= carr N

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (H,N) or x in carr N )
assume x in commutators (H,N) ; :: thesis: x in carr N
then consider a, b being Element of G such that
A1: x = [.a,b.] and
a in H and
A2: b in N by Th52;
b " in N by A2, GROUP_2:51;
then (b ") |^ a in N |^ a by GROUP_3:58;
then (b ") |^ a in N by GROUP_3:def 13;
then x in N by A1, A2, GROUP_2:50;
hence x in carr N by STRUCT_0:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (N,H) or x in carr N )
assume x in commutators (N,H) ; :: thesis: x in carr N
then consider a, b being Element of G such that
A3: x = [.a,b.] and
A4: a in N and
b in H by Th52;
a |^ b in N |^ b by A4, GROUP_3:58;
then A5: a |^ b in N by GROUP_3:def 13;
( x = (a ") * (a |^ b) & a " in N ) by A3, A4, Th16, GROUP_2:51;
then x in N by A5, GROUP_2:50;
hence x in carr N by STRUCT_0:def 5; :: thesis: verum