:: deftheorem defines + RINGFRAC:def 12 :
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 = Fracadd (x,y);