let R be Ring; :: thesis: for y being Element of R holds
( y in center R iff for s being Element of R holds y * s = s * y )
let y be Element of R; :: thesis: ( y in center R iff for s being Element of R holds y * s = s * y )

hereby :: thesis: ( ( for s being Element of R holds y * s = s * y ) implies y in center R )

assume y in center R ; :: thesis: for s being Element of R holds y * s = s * y
then y in the carrier of (center R) ;
then y in { x where x is Element of R : for s being Element of R holds x * s = s * x } by Def4;
then ex x being Element of R st
( x = y & ( for s being Element of R holds x * s = s * x ) ) ;
hence for s being Element of R holds y * s = s * y ; :: thesis: verum

end;

now :: thesis: ( ( for s being Element of R holds y * s = s * y ) implies y in center R )

assume for s being Element of R holds y * s = s * y ; :: thesis: y in center R
then y in { x where x is Element of R : for s being Element of R holds x * s = s * x } ;
then y is Element of (center R) by Def4;
hence y in center R ; :: thesis: verum

end;

hence ( ( for s being Element of R holds y * s = s * y ) implies y in center R ) ; :: thesis: verum