defpred S1[ object , object ] means ex u, v being Element of Frac S st
( u = $1 & v = $2 & u,v Fr_Eq S );
A1: for o, o1 being object st S1[o,o1] holds
S1[o1,o] by Th23;
A2: for o, o1, o2 being object st S1[o,o1] & S1[o1,o2] holds
S1[o,o2] by Th24;
A3: for o being object st o in Frac S holds
S1[o,o] by Th22;
consider ER being Equivalence_Relation of (Frac S) such that
A4: for o, o1 being object holds
( [o,o1] in ER iff ( o in Frac S & o1 in Frac S & S1[o,o1] ) ) from EQREL_1:sch 1(A3, A1, A2);
 take ER ; :: thesis: for u, v being Element of Frac S holds
( [u,v] in ER iff u,v Fr_Eq S )
for u, v being Element of Frac S holds
( [u,v] in ER iff u,v Fr_Eq S )
proof
let u, v be Element of Frac S; :: thesis: ( [u,v] in ER iff u,v Fr_Eq S )
thus ( [u,v] in ER implies u,v Fr_Eq S ) :: thesis: ( u,v Fr_Eq S implies [u,v] in ER )
proof
assume [u,v] in ER ; :: thesis: u,v Fr_Eq S
then ex u1, v1 being Element of Frac S st
( u1 = u & v1 = v & u1,v1 Fr_Eq S ) by A4;
hence u,v Fr_Eq S ; :: thesis: verum
end;
assume u,v Fr_Eq S ; :: thesis: [u,v] in ER
hence [u,v] in ER by A4; :: thesis: verum
end;
hence for u, v being Element of Frac S holds
( [u,v] in ER iff u,v Fr_Eq S ) ; :: thesis: verum