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