theorem Th34: :: RINGFRAC:27

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of (S ~ R) holds x * y = y * x