let G be Group; :: thesis: for N, N1, N2 being normal Subgroup of G st N1 is Subgroup of N2 holds
ex N3, N4 being strict normal Subgroup of G st
( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 )
let N, N1, N2 be normal Subgroup of G; :: thesis: ( N1 is Subgroup of N2 implies ex N3, N4 being strict normal Subgroup of G st
( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 ) )
assume A1: N1 is Subgroup of N2 ; :: thesis: ex N3, N4 being strict normal Subgroup of G st
( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 )
consider N3 being strict normal Subgroup of G such that
A2: the carrier of N3 = N ~ N1 by Th73;
consider N4 being strict normal Subgroup of G such that
A3: the carrier of N4 = N ~ N2 by Th73;
N3 is Subgroup of N4 by A1, A2, A3, Th56, GROUP_2:57;
then N3 ~ N1 c= N4 ~ N1 by Th57;
hence ex N3, N4 being strict normal Subgroup of G st
( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 ) by A2, A3; :: thesis: verum