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

proof

assume a in center G ; :: thesis: for b being Element of 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 : for c being Element of holds b * c = c * b } by Def10;
then ex b being Element of st
( a = b & ( for c being Element of holds b * c = c * b ) ) ;
hence for b being Element of holds a * b = b * a ; :: thesis: verum

end;

assume for b being Element of holds a * b = b * a ; :: thesis: a in center G
then a in { c where c is Element of : for b being Element of 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