let R be Skew-Field; :: 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

for s being Element of R holds (1_ R) * s = s * (1_ R) ;

hence 1_ R in center R by Th17; :: thesis: verum