:: deftheorem Def14 defines Normalizer GROUP_1A:def 42 :
for G being addGroup
for A being Subset of G
for b₃ being strict Subgroup of G holds
( b₃ = Normalizer A iff the carrier of b₃ = { h where h is Element of G : A * h = A } );