let G be Group; :: thesis: for A being non empty Subset 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 ~ A) \/ (N2 ~ A) c= N ~ A )

let A be non empty Subset 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 ~ A) \/ (N2 ~ A) c= N ~ A )

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 ~ A) \/ (N2 ~ A) c= N ~ A )

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 ~ A c= N ~ A & N2 ~ A c= N ~ A ) by Th26;

(N1 ~ A) \/ (N2 ~ A) c= N ~ A

( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A ) by A1; :: thesis: verum

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 ~ A) \/ (N2 ~ A) c= N ~ A )

let A be non empty Subset 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 ~ A) \/ (N2 ~ A) c= N ~ A )

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 ~ A) \/ (N2 ~ A) c= N ~ A )

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 ~ A c= N ~ A & N2 ~ A c= N ~ A ) by Th26;

(N1 ~ A) \/ (N2 ~ A) c= N ~ A

proof

hence
ex N being strict normal Subgroup of G st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N1 ~ A) \/ (N2 ~ A) or x in N ~ A )

assume x in (N1 ~ A) \/ (N2 ~ A) ; :: thesis: x in N ~ A

then ( x in N1 ~ A or x in N2 ~ A ) by XBOOLE_0:def 3;

hence x in N ~ A by A2; :: thesis: verum

end;assume x in (N1 ~ A) \/ (N2 ~ A) ; :: thesis: x in N ~ A

then ( x in N1 ~ A or x in N2 ~ A ) by XBOOLE_0:def 3;

hence x in N ~ A by A2; :: thesis: verum

( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A ) by A1; :: thesis: verum