theorem Th32: :: RINGFRAC:25

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