:: deftheorem defines 1. RINGFRAC:def 17 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds 1. (R,S) = [(1. R),(1. R)];