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

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