let R be commutative Ring; :: thesis: for x being object st x in R holds
x in center R
let x be object ; :: thesis: ( x in R implies x in center R )
assume x in R ; :: thesis: x in center R
then reconsider x9 = x as Element of R by STRUCT_0:def 5;
for y9 being Element of R holds x9 * y9 = y9 * x9 ;
hence x in center R by WEDDWITT:17; :: thesis: verum