theorem ThJoinNormUnionRes: :: GROUP_23:81

for G being Group
for I being set
for J being Subset of I
for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier (F | J)) holds
ex N being strict normal Subgroup of G st N = gr A