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