let G be 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 )
let N, N1 be normal Subgroup of G; ( 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 & N3 ~ N c= N2 ~ N ) )
assume A1:
N1 is Subgroup of N
; 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 )
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
N3 ~ N c= N2 ~ N
by Th57;
hence
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 )
by A2, A3; verum