let G be Group; :: thesis: for a being Element of G
for x being set st x in Centralizer a holds
x in G
let a be Element of G; :: thesis: for x being set st x in Centralizer a holds
x in G
let x be set ; :: thesis: ( x in Centralizer a implies x in G )
assume A1: x in Centralizer a ; :: thesis: x in G
the carrier of (Centralizer a) = { b where b is Element of G : a * b = b * a } by Def1;
then x in { b where b is Element of G : a * b = b * a } by A1, STRUCT_0:def 5;
then ex b being Element of G st
( b = x & a * b = b * a ) ;
hence x in G by STRUCT_0:def 5; :: thesis: verum