let A, B be Relation of R; :: thesis: ( ( for a, b being Element of R holds
( [a,b] in A iff a - b in I ) ) & ( for a, b being Element of R holds
( [a,b] in B iff a - b in I ) ) implies A = B )
assume that
A2: for a, b being Element of R holds
( [a,b] in A iff a - b in I ) and
A3: for a, b being Element of R holds
( [a,b] in B iff a - b in I ) ; :: thesis: A = B
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in A or [x,y] in B ) & ( not [x,y] in B or [x,y] in A ) )
thus ( [x,y] in A implies [x,y] in B ) :: thesis: ( not [x,y] in B or [x,y] in A )

proof

assume A4: [x,y] in A ; :: 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, A4;
hence [x,y] in B by A3; :: thesis: verum

end;

assume A5: [x,y] in B ; :: thesis: [x,y] in A
then reconsider x = x, y = y as Element of R by ZFMISC_1:87;
x - y in I by A3, A5;
hence [x,y] in A by A2; :: thesis: verum