let G be Group; :: thesis: 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 & N2 ` N c= N3 ` N )

let N, N1 be normal Subgroup of G; :: thesis: ( N1 is Subgroup of N implies ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) )

assume A1: N1 is Subgroup of N ; :: thesis: ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N )

consider N2 being strict normal Subgroup of G such that

A2: the carrier of N2 = N1 ~ N by Th73;

consider N3 being strict normal Subgroup of G such that

A3: the carrier of N3 = N1 ` N by A1, Th74;

N3 is Subgroup of N2 by A2, A3, Th55, GROUP_2:57;

then N2 ` N c= N3 ` N by Th60;

hence ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) by A2, A3; :: thesis: verum

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N )

let N, N1 be normal Subgroup of G; :: thesis: ( N1 is Subgroup of N implies ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) )

assume A1: N1 is Subgroup of N ; :: thesis: ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N )

consider N2 being strict normal Subgroup of G such that

A2: the carrier of N2 = N1 ~ N by Th73;

consider N3 being strict normal Subgroup of G such that

A3: the carrier of N3 = N1 ` N by A1, Th74;

N3 is Subgroup of N2 by A2, A3, Th55, GROUP_2:57;

then N2 ` N c= N3 ` N by Th60;

hence ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) by A2, A3; :: thesis: verum