:: deftheorem defines Normalizer GROUP_3:def 15 :
for G being Group
for H being Subgroup of G holds Normalizer H = Normalizer (carr H);