theorem Th129: :: GROUP_1A:328

for x being set
for G being addGroup
for A being Subset of G holds
( x in Normalizer A iff ex h being Element of G st
( x = h & A * h = A ) )