theorem Th15: :: RINGFRAC:11

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds Frac S = [:([#] R),S:]