:: deftheorem defines Fr_Eq RINGFRAC:def 14 :
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,y Fr_Eq S iff ex s1 being Element of R st
( s1 in S & (((x `1) * (y `2)) - ((y `1) * (x `2))) * s1 = 0. R ) );