let R be Ring; :: thesis: ( center R is commutative & center R is Subring of R )
thus center R is commutative ; :: thesis: center R is Subring of R
A1: for x being object st x in the carrier of (center R) holds
x in the carrier of R

proof

let x be object ; :: thesis: ( x in the carrier of (center R) implies x in the carrier of R )
assume x in the carrier of (center R) ; :: thesis: x in the carrier of R
then reconsider r = x as Element of (center R) ;
r is Element of R by WEDDWITT:41;
hence x in the carrier of R ; :: thesis: verum

end;

( the addF of (center R) = the addF of R || the carrier of (center R) & the multF of (center R) = the multF of R || the carrier of (center R) & 0. (center R) = 0. R & 1. (center R) = 1. R ) by WEDDWITT:def 4;
hence center R is Subring of R by A1, C0SP1:def 3, TARSKI:def 3; :: thesis: verum