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 is Subgroup of N & N2 is Subgroup of N ) by A1, Th9;
then A2: ( N1 ~ H c= N ~ H & N2 ~ H c= N ~ H ) by Th57;
(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 x in (N1 ~ H) \/ (N2 ~ H) ; :: thesis: x in N ~ H
then ( x in N1 ~ H or x in N2 ~ H ) by XBOOLE_0:def 3;
hence x in N ~ H by A2; :: 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