let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x, y being Element of (S ~ R) holds x * y = y * x
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x, y being Element of (S ~ R) holds x * y = y * x
let x, y be Element of (S ~ R); :: thesis: x * y = y * x
consider a being Element of Frac S such that
A1: x = Class ((EqRel S),a) by Th32;
consider b being Element of Frac S such that
A2: y = Class ((EqRel S),b) by Th32;
x * y = Class ((EqRel S),(a * b)) by A1, A2, Th33
.= Class ((EqRel S),(b * a))
.= y * x by A1, A2, Th33 ;
hence x * y = y * x ; :: thesis: verum