set A = EqRel (R,I);

consider B being Equivalence_Relation of the carrier of R such that

A1: for x, y being object 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

consider B being Equivalence_Relation of the carrier of R such that

A1: for x, y being object 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

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:9, RELAT_1:40; :: thesis: verum
let x, y be object ; :: 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) )

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;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
[x,y] in B
; :: thesis: [x,y] in EqRel (R,I)
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:87;

x - y in I by A2, Def5;

hence [x,y] in B by A1; :: thesis: verum

end;then reconsider x = x, y = y as Element of R by ZFMISC_1:87;

x - y in I by A2, Def5;

hence [x,y] in B by A1; :: thesis: verum

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