let G be Group; 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; 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; ( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
thus
commutators (H,N) c= carr N
commutators (N,H) c= carr N
let x be object ; TARSKI:def 3 ( not x in commutators (N,H) or x in carr N )
assume
x in commutators (N,H)
; 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; verum