theorem Th73: :: GROUP_11:73

for G being Group
for H, N being normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N ~ H