:: deftheorem Def6 defines FracRing RINGFRAC:def 18 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for b₃ being strict doubleLoopStr holds
( b₃ = FracRing S iff ( the carrier of b₃ = Class (EqRel S) & 1. b₃ = Class ((EqRel S),(1. (R,S))) & 0. b₃ = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b₃ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b₃ . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b₃ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b₃ . (x,y) = Class ((EqRel S),(a * b)) ) ) ) );