theorem Th80: :: GROUP_22:75

for G being Group
for H being Subgroup of G holds H is Subgroup of Normalizer H