theorem Th57: :: GROUP_22:55

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