theorem :: GROUP_23:82

for G being Group
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