theorem :: GROUP_11:80

for G being Group
for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st
( the carrier of N2 = N ` N & N ` N1 c= N2 ` N1 )