theorem :: GROUP_22:62

for G being Group
for A being non empty Subset of G holds the carrier of (Centralizer A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & ex a being Element of G st
( a in A & H = Normalizer a ) ) }