:: deftheorem Def18 defines normal GROUP_23:def 19 :
for I being set
for G being Group
for IT being Subgroup-Family of I,G holds
( IT is normal iff for i being object st i in I holds
IT . i is normal Subgroup of G );