let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for s being Element of S holds Class ((EqRel S),[s,(1. R)]) is Unit of (S ~ R)
let S be non empty multiplicatively-closed Subset of R; :: thesis: for s being Element of S holds Class ((EqRel S),[s,(1. R)]) is Unit of (S ~ R)
let s be Element of S; :: thesis: Class ((EqRel S),[s,(1. R)]) is Unit of (S ~ R)
1. R in S by C0SP1:def 4;
then reconsider a = [s,(1. R)] as Element of Frac S by Def3;
a `1 in S ;
hence Class ((EqRel S),[s,(1. R)]) is Unit of (S ~ R) by Lm45; :: thesis: verum