let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x being Element of (S ~ R) ex a being Element of Frac S st x = Class ((EqRel S),a)
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x being Element of (S ~ R) ex a being Element of Frac S st x = Class ((EqRel S),a)
let x be Element of (S ~ R); :: thesis: ex a being Element of Frac S st x = Class ((EqRel S),a)
the carrier of (S ~ R) = Class (EqRel S) by Def6;
then x in Class (EqRel S) ;
then ex a being object st
( a in Frac S & x = Class ((EqRel S),a) ) by EQREL_1:def 3;
hence ex a being Element of Frac S st x = Class ((EqRel S),a) ; :: thesis: verum