:: deftheorem Def3 defines Frac RINGFRAC:def 8 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for b₃ being Subset of [: the carrier of R, the carrier of R:] holds
( b₃ = Frac S iff for x being set holds
( x in b₃ iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) );