theorem :: GROUP_22:76

for G being Group
for H being Subgroup of G holds Centralizer H is strict normal Subgroup of Normalizer H