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 & N3 ` N c= N2 ~ 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 & N3 ` N c= N2 ~ N ) )
assume 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 & N3 ` N c= N2 ~ N )
then consider N2, N3 being strict normal Subgroup of G such that
A1: the carrier of N2 = N1 ~ N and
A2: the carrier of N3 = N1 ` N and
A3: N3 ~ N c= N2 ~ N by Th76;
N3 ` N c= N3 ~ N by Th55;
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 A1, A2, A3, XBOOLE_1:1; :: thesis: verum