theorem :: GROUP_11:48

for G being Group
for A being non empty Subset of G
for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )