let G be Group; :: thesis: for a being Element of G holds
( a in center G iff for b being Element of G holds a * b = b * a )
let a be Element of G; :: thesis: ( a in center G iff for b being Element of G holds a * b = b * a )
thus ( a in center G implies for b being Element of G holds a * b = b * a ) :: thesis: ( ( for b being Element of G holds a * b = b * a ) implies a in center G )

proof

assume a in center G ; :: thesis: for b being Element of G holds a * b = b * a
then a in the carrier of (center G) by STRUCT_0:def 5;
then a in { b where b is Element of G : for c being Element of G holds b * c = c * b } by Def10;
then ex b being Element of G st
( a = b & ( for c being Element of G holds b * c = c * b ) ) ;
hence for b being Element of G holds a * b = b * a ; :: thesis: verum

end;

assume for b being Element of G holds a * b = b * a ; :: thesis: a in center G
then a in { c where c is Element of G : for b being Element of G holds c * b = b * c } ;
then a in the carrier of (center G) by Def10;
hence a in center G by STRUCT_0:def 5; :: thesis: verum