theorem :: GROUP_6:80

for G being Group
for N being normal Subgroup of G
for M being strict normal Subgroup of G
for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic