let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for z being Element of (S ~ R) ex r1, r2 being Element of R st
( r2 in S & z = Class ((EqRel S),[r1,r2]) )
let S be non empty multiplicatively-closed Subset of R; :: thesis: for z being Element of (S ~ R) ex r1, r2 being Element of R st
( r2 in S & z = Class ((EqRel S),[r1,r2]) )
let z be Element of (S ~ R); :: thesis: ex r1, r2 being Element of R st
( r2 in S & z = Class ((EqRel S),[r1,r2]) )
consider r being Element of Frac S such that
A1: z = Class ((EqRel S),r) by Th32;
consider r1, r2 being Element of R such that
A2: r1 = r `1 and
A3: r2 = r `2 ;
z = Class ((EqRel S),[r1,r2]) by A1, A2, A3;
hence ex r1, r2 being Element of R st
( r2 in S & z = Class ((EqRel S),[r1,r2]) ) by A3, Lm17; :: thesis: verum