theorem :: GROUP_23:80

for G being Group
for I being set
for J being Subset of I st J is empty holds
for F being normal Subgroup-Family of I,G holds Carrier (F | J) = {} --> (bool the carrier of G) ;