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

proof

let x be object ; :: thesis: ( x in the carrier of (center R) iff x in the carrier of R )

hereby :: thesis: ( x in the carrier of R implies x in the carrier of (center R) )

assume A1: x in the carrier of (center R) ; :: thesis: x in the carrier of R
the carrier of (center R) c= the carrier of R by C0SP1:def 3;
hence x in the carrier of R by A1; :: thesis: verum

end;

assume x in the carrier of R ; :: thesis: x in the carrier of (center R)
then reconsider x9 = x as Element of R ;
x9 in center R by Th14;
hence x in the carrier of (center R) by STRUCT_0:def 5; :: thesis: verum

end;

hence the carrier of (center R) = the carrier of R by TARSKI:2; :: thesis: verum