let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x being object st x in the carrier of R holds
[x,(1. R)] in Frac S
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x being object st x in the carrier of R holds
[x,(1. R)] in Frac S
let x be object ; :: thesis: ( x in the carrier of R implies [x,(1. R)] in Frac S )
assume x in the carrier of R ; :: thesis: [x,(1. R)] in Frac S
then reconsider x = x as Element of R ;
1. R in S by C0SP1:def 4;
then [x,(1. R)] in Frac S by Def3;
hence [x,(1. R)] in Frac S ; :: thesis: verum