let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S st 0. R in S holds
x,y Fr_Eq S
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x, y being Element of Frac S st 0. R in S holds
x,y Fr_Eq S
let x, y be Element of Frac S; :: thesis: ( 0. R in S implies x,y Fr_Eq S )
assume A1: 0. R in S ; :: thesis: x,y Fr_Eq S
reconsider s1 = 0. R as Element of R ;
A2: (((x `1) * (y `2)) - ((y `1) * (x `2))) * s1 = 0. R ;
reconsider s1 = s1 as Element of S by A1;
thus x,y Fr_Eq S by A1, A2; :: thesis: verum