theorem Th64: :: GROUP_22:61

for G being Group
for a, x being Element of G holds
( x in Normalizer a iff ex h being Element of G st
( x = h & a |^ h = a ) )