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 ) ; :: thesis: ( ( 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 ; :: thesis: R c= Z

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

assume A2: [a,b] in R ; :: thesis: [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 ; :: thesis: verum

for y being Element of Y st [x,y] in R holds

[x,y] in Z ) ; :: thesis: ( ( 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 ; :: thesis: R c= Z

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

assume A2: [a,b] in R ; :: thesis: [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 ; :: thesis: verum