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;

then ex b being Element of G st

( b = x & a * b = b * a ) ;

hence x in G ; :: thesis: verum

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;

then ex b being Element of G st

( b = x & a * b = b * a ) ;

hence x in G ; :: thesis: verum