theorem Th33: :: RINGFRAC:26

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for a, b being Element of Frac S
for x, y being Element of (S ~ R) st x = Class ((EqRel S),a) & y = Class ((EqRel S),b) holds
x * y = Class ((EqRel S),(a * b))