set A = EqRel R,I;
consider B being Equivalence_Relation of the carrier of R such that
A1: for x, y being set holds
( [x,y] in B iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) ) ) by Lm1;
EqRel R,I = B

proof

let x, y be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in EqRel R,I or [x,y] in B ) & ( not [x,y] in B or [x,y] in EqRel R,I ) )
thus ( [x,y] in EqRel R,I implies [x,y] in B ) :: thesis: ( not [x,y] in B or [x,y] in EqRel R,I )

proof

assume A2: [x,y] in EqRel R,I ; :: thesis: [x,y] in B
then reconsider x = x, y = y as Element of R by ZFMISC_1:106;
x - y in I by A2, Def5;
hence [x,y] in B by A1; :: thesis: verum

end;

assume [x,y] in B ; :: thesis: [x,y] in EqRel R,I
then ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) by A1;
hence [x,y] in EqRel R,I by Def5; :: thesis: verum

end;

hence ( not EqRel R,I is empty & EqRel R,I is total & EqRel R,I is symmetric & EqRel R,I is transitive ) by EQREL_1:16, RELAT_1:63; :: thesis: verum