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 )

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

( [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 A5:
[x,y] in B
; :: thesis: [x,y] in A
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;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

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