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 )

N is Subgroup of N by GROUP_2:54;

then consider N2 being strict normal Subgroup of G such that

A1: the carrier of N2 = N ` N by Th74;

N2 is Subgroup of N by A1, Th53, GROUP_2:57;

then N ` N1 c= N2 ` N1 by Th60;

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

( 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 )

N is Subgroup of N by GROUP_2:54;

then consider N2 being strict normal Subgroup of G such that

A1: the carrier of N2 = N ` N by Th74;

N2 is Subgroup of N by A1, Th53, GROUP_2:57;

then N ` N1 c= N2 ` N1 by Th60;

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