:: deftheorem Def5 defines EqRel RINGFRAC:def 15 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for b₃ being Equivalence_Relation of (Frac S) holds
( b₃ = EqRel S iff for u, v being Element of Frac S holds
( [u,v] in b₃ iff u,v Fr_Eq S ) );