theorem :: GROUP_22:71

for G being Group
for H being Subgroup of G holds
( H is Subgroup of Centralizer H iff H is commutative Group )