let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x being Element of Frac S holds
( x `1 in R & x `2 in S )
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x being Element of Frac S holds
( x `1 in R & x `2 in S )
let x be Element of Frac S; :: thesis: ( x `1 in R & x `2 in S )
x in Frac S ;
then x in [:([#] R),S:] by Th15;
hence ( x `1 in R & x `2 in S ) by MCART_1:10; :: thesis: verum