for x, y being Element of (center R) holds x + y = y + x

proof

let x, y be Element of (center R); :: thesis: x + y = y + x
reconsider a = x, b = y as Element of R by Lm1;
thus x + y = a + b by Lm2
.= b + a
.= y + x by Lm2 ; :: thesis: verum

end;

hence center R is Abelian by RLVECT_1:def 2; :: thesis: verum