theorem Th59: :: GROUP_22:57

for G being Group
for H being Subgroup of G holds the carrier of (Centralizer H) = { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b }