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
( x in 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
( x in Class ((EqRel S),y) iff x,y Fr_Eq S )
let x, y be Element of Frac S; :: thesis: ( x in Class ((EqRel S),y) iff x,y Fr_Eq S )
set E = EqRel S;

hereby :: thesis: ( x,y Fr_Eq S implies x in Class ((EqRel S),y) )

assume x in Class ((EqRel S),y) ; :: thesis: x,y Fr_Eq S
then [x,y] in EqRel S by EQREL_1:19;
hence x,y Fr_Eq S by Def5; :: thesis: verum

end;

assume x,y Fr_Eq S ; :: thesis: x in Class ((EqRel S),y)
then [x,y] in EqRel S by Def5;
hence x in Class ((EqRel S),y) by EQREL_1:19; :: thesis: verum