theorem :: GROUP_5:67
for G being Group
for H being Subgroup of G
for N being strict normal Subgroup of G holds
( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )