theorem Th60: :: GROUP_22:58

for G being Group
for H being Subgroup of G
for g being Element of G holds
( ( for a being Element of G st a in H holds
g * a = a * g ) iff g is Element of (Centralizer H) )