theorem Th137: :: GROUP_1A:336

for G being strict addGroup
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff Normalizer H = G )