theorem Th25: :: RINGFRAC:18

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S holds
( x in Class ((EqRel S),y) iff x,y Fr_Eq S )