theorem Th46: :: RINGFRAC:30

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for z being Element of (S ~ R) ex r1, r2 being Element of R st
( r2 in S & z = Class ((EqRel S),[r1,r2]) )