let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R holds Class ((EqRel S),((frac1 S) . (1. R))) = 1. (S ~ R)
let S be non empty multiplicatively-closed Subset of R; :: thesis: Class ((EqRel S),((frac1 S) . (1. R))) = 1. (S ~ R)
reconsider a = (frac1 S) . (1. R) as Element of Frac S ;
A1: (frac1 S) . (1. R) = [(1. R),(1. R)] by Def4;
a `1 = a `2 by A1;
hence Class ((EqRel S),((frac1 S) . (1. R))) = 1. (S ~ R) by Lm42; :: thesis: verum