:: deftheorem Def13 defines normal GROUP_1A:def 41 :
for G being addGroup
for IT being Subgroup of G holds
( IT is normal iff for a being Element of G holds IT * a = addMagma(# the carrier of IT, the addF of IT #) );