consider E being Equivalence_Relation of such that
A1: for x, y being set holds
( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of st
( P = x & Q = y & P - Q in I ) ) ) by Lm1;
take E ; :: thesis: for a, b being Element of holds
( [a,b] in E iff a - b in I )
let a, b be Element of ; :: thesis: ( [a,b] in E iff a - b in I )
thus ( [a,b] in E implies a - b in I ) :: thesis: ( a - b in I implies [a,b] in E )

proof

assume [a,b] in E ; :: thesis: a - b in I
then ex P, Q being Element of st
( P = a & Q = b & P - Q in I ) by A1;
hence a - b in I ; :: thesis: verum

end;

thus ( a - b in I implies [a,b] in E ) by A1; :: thesis: verum