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 set ; :: 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 Th58;
b " in N by A2, GROUP_2:60;
then (b " ) |^ a in N |^ a by GROUP_3:70;
then (b " ) |^ a in N by GROUP_3:def 13;
then x in N by A1, A2, GROUP_2:59;
hence x in carr N by STRUCT_0:def 5; :: thesis: verum

end;

let x be set ; :: 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 Th58;
a |^ b in N |^ b by A4, GROUP_3:70;
then A5: a |^ b in N by GROUP_3:def 13;
( x = (a " ) * (a |^ b) & a " in N ) by A3, A4, Th19, GROUP_2:60;
then x in N by A5, GROUP_2:59;
hence x in carr N by STRUCT_0:def 5; :: thesis: verum