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
proof
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) )
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:87;
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:9, RELAT_1:40; :: thesis: verum