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