theorem ThS1: :: GROUP_23:69

for I being non empty set
for G being Group
for F being Subgroup-Family of I,G holds
( F is normal iff for i being Element of I holds F . i is normal Subgroup of G ) ;