let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for u being Element of Frac S holds u `2 in S
let S be non empty multiplicatively-closed Subset of R; :: thesis: for u being Element of Frac S holds u `2 in S
let u be Element of Frac S; :: thesis: u `2 in S
ex a, b being Element of R st
( u = [a,b] & b in S ) by Def3;
hence u `2 in S ; :: thesis: verum