consider E being Equivalence_Relation of the carrier of R such that

A1: for x, y being object holds

( [x,y] in E 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;

take E ; :: thesis: for a, b being Element of R holds

( [a,b] in E iff a - b in I )

let a, b be Element of R; :: 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 )

A1: for x, y being object holds

( [x,y] in E 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;

take E ; :: thesis: for a, b being Element of R holds

( [a,b] in E iff a - b in I )

let a, b be Element of R; :: 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

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

then ex P, Q being Element of R st

( P = a & Q = b & P - Q in I ) by A1;

hence a - b in I ; :: thesis: verum

end;then ex P, Q being Element of R st

( P = a & Q = b & P - Q in I ) by A1;

hence a - b in I ; :: thesis: verum