:: deftheorem Def1 defines Centralizer WEDDWITT:def 1 :
for G being Group
for a being Element of G
for b₃ being strict Subgroup of G holds
( b₃ = Centralizer a iff the carrier of b₃ = { b where b is Element of G : a * b = b * a } );