theorem Th134: :: GROUP_1A:333

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