let R be Ring; :: thesis: the carrier of (center R) c= the carrier of R
for x being object st x in the carrier of (center R) holds
x in the carrier of R

proof

let y be object ; :: thesis: ( y in the carrier of (center R) implies y in the carrier of R )
assume y in the carrier of (center R) ; :: thesis: y in the carrier of 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 y in the carrier of R ; :: thesis: verum

end;

hence the carrier of (center R) c= the carrier of R ; :: thesis: verum