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 )
proof
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;
thus ( a - b in I implies [a,b] in E ) by A1; :: thesis: verum