thus
( R c= Z implies for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z )
; ( ( for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z ) implies R c= Z )
assume A1:
for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z
; R c= Z
let a, b be object ; RELAT_1:def 3 ( not [a,b] in R or [a,b] in Z )
assume A2:
[a,b] in R
; [a,b] in Z
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 Z
by A1, A2;
hence
[a,b] in Z
; verum