let R be Skew-Field; :: 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) by STRUCT_0:def 5;
then y in { x where x is Element of R : for s being Element of R holds x * s = s * x } by Def4;
then consider x being Element of R such that
A1: x = y and
A2: for s being Element of R holds x * s = s * x ;
thus for s being Element of R holds y * s = s * y by A1, A2; :: thesis: verum

end;

now

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 by STRUCT_0:def 5; :: thesis: verum

end;

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