:: deftheorem Def7 defines normal GROUP_23:def 6 :
for I being non empty set
for F being Group-Family of I
for IT being Subgroup-Family of F holds
( IT is normal iff for i being Element of I holds IT . i is normal Subgroup of F . i );