let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S holds
( Class ((EqRel S),x) = Class ((EqRel S),y) iff x,y Fr_Eq S )
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x, y being Element of Frac S holds
( Class ((EqRel S),x) = Class ((EqRel S),y) iff x,y Fr_Eq S )
let x, y be Element of Frac S; :: thesis: ( Class ((EqRel S),x) = Class ((EqRel S),y) iff x,y Fr_Eq S )
set E = EqRel S;
thus ( Class ((EqRel S),x) = Class ((EqRel S),y) implies x,y Fr_Eq S ) :: thesis: ( x,y Fr_Eq S implies Class ((EqRel S),x) = Class ((EqRel S),y) )

proof

assume Class ((EqRel S),x) = Class ((EqRel S),y) ; :: thesis: x,y Fr_Eq S
then x in Class ((EqRel S),y) by EQREL_1:23;
hence x,y Fr_Eq S by Th25; :: thesis: verum

end;

assume x,y Fr_Eq S ; :: thesis: Class ((EqRel S),x) = Class ((EqRel S),y)
then x in Class ((EqRel S),y) by Th25;
hence Class ((EqRel S),x) = Class ((EqRel S),y) by EQREL_1:23; :: thesis: verum