let R be commutative Ring; :: thesis: for x being Element of R holds x in center R
let x be Element of R; :: thesis: x in center R
for y being Element of R holds x * y = y * x ;
hence x in center R by WEDDWITT:17; :: thesis: verum