let G be Group; :: thesis: for H being Subgroup of G
for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )
let H be Subgroup of G; :: thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )
let N1, N2 be strict normal Subgroup of G; :: thesis: ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )
consider N being strict normal Subgroup of G such that
A1: the carrier of N = N1 * N2 by Th8;
(N1 ~ H) * (N2 ~ H) c= N ~ H

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N1 ~ H) * (N2 ~ H) or x in N ~ H )
assume A2: x in (N1 ~ H) * (N2 ~ H) ; :: thesis: x in N ~ H
then reconsider x = x as Element of G ;
consider a, b being Element of G such that
A3: ( x = a * b & a in N1 ~ H & b in N2 ~ H ) by A2;
A4: a * N1 meets carr H by A3, Th51;
A5: b * N2 meets carr H by A3, Th51;
consider x1 being object such that
A6: ( x1 in a * N1 & x1 in carr H ) by A4, XBOOLE_0:3;
consider x2 being object such that
A7: ( x2 in b * N2 & x2 in carr H ) by A5, XBOOLE_0:3;
reconsider x1 = x1 as Element of G by A6;
reconsider x2 = x2 as Element of G by A7;
A8: x1 * x2 in (carr H) * (carr H) by A6, A7;
A9: x1 * x2 in (a * N1) * (b * N2) by A6, A7;
(carr H) * (carr H) = carr H by GROUP_2:76;
then A10: (a * N1) * (b * N2) meets carr H by A8, A9, XBOOLE_0:3;
(a * N1) * (b * N2) = (a * b) * N by A1, Th10;
hence x in N ~ H by A3, A10; :: thesis: verum

end;

hence ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H ) by A1; :: thesis: verum