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 ) )
; ( ( 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 )
; P = R
let a, b be object ; RELAT_1:def 2 ( ( not [a,b] in P or [a,b] in R ) & ( not [a,b] in R or [a,b] in P ) )
hereby ( not [a,b] in R or [a,b] in P )
end;
assume A3:
[a,b] in R
; [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
; verum