:: deftheorem Def5 defines Centralizer GROUP_22:def 6 :
for G being Group
for H being Subgroup of G
for b₃ being strict Subgroup of G holds
( b₃ = Centralizer H iff b₃ = Centralizer (carr H) );