let R be Ring; :: thesis: 1_ R in center R
for s being Element of R holds (1_ R) * s = s * (1_ R) ;
hence 1_ R in center R by Th17; :: thesis: verum