let G be Group; :: thesis: for I being set
for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier F) holds
ex N being strict normal Subgroup of G st N = gr A
let I be set ; :: thesis: for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier F) holds
ex N being strict normal Subgroup of G st N = gr A
let F be normal Subgroup-Family of I,G; :: thesis: for A being Subset of G st A = Union (Carrier F) holds
ex N being strict normal Subgroup of G st N = gr A
let A be Subset of G; :: thesis: ( A = Union (Carrier F) implies ex N being strict normal Subgroup of G st N = gr A )
assume A1: A = Union (Carrier F) ; :: thesis: ex N being strict normal Subgroup of G st N = gr A
reconsider J = [#] I as Subset of I ;
I = J by SUBSET_1:def 3;
then A = Union (Carrier (F | J)) by A1;
hence ex N being strict normal Subgroup of G st N = gr A by ThJoinNormUnionRes; :: thesis: verum