thus
( P = R implies for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) ) ; :: thesis: ( ( for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) ) implies P = R )

assume A1: for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) ; :: thesis: P = R

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in P or [a,b] in R ) & ( not [a,b] in R or [a,b] in P ) )

then reconsider a9 = a as Element of X by ZFMISC_1:87;

reconsider b9 = b as Element of Y by A3, ZFMISC_1:87;

[a9,b9] in P by A1, A3;

hence [a,b] in P ; :: thesis: verum

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) ) ; :: thesis: ( ( for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) ) implies P = R )

assume A1: for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) ; :: thesis: P = R

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in P or [a,b] in R ) & ( not [a,b] in R or [a,b] in P ) )

hereby :: thesis: ( not [a,b] in R or [a,b] in P )

assume A3:
[a,b] in R
; :: thesis: [a,b] in Passume A2:
[a,b] in P
; :: thesis: [a,b] in R

then reconsider a9 = a as Element of X by ZFMISC_1:87;

reconsider b9 = b as Element of Y by A2, ZFMISC_1:87;

[a9,b9] in R by A1, A2;

hence [a,b] in R ; :: thesis: verum

end;then reconsider a9 = a as Element of X by ZFMISC_1:87;

reconsider b9 = b as Element of Y by A2, ZFMISC_1:87;

[a9,b9] in R by A1, A2;

hence [a,b] in R ; :: thesis: verum

then reconsider a9 = a as Element of X by ZFMISC_1:87;

reconsider b9 = b as Element of Y by A3, ZFMISC_1:87;

[a9,b9] in P by A1, A3;

hence [a,b] in P ; :: thesis: verum