for G being Group
for a, x being Element of G holds
( a * x = x * a iff x is Element of (Centralizer a) )