now :: thesis: for x, z being object st [x,z] in P * R holds

[x,z] in [:X,Z:]

hence
P * R is Relation of X,Z
by RELAT_1:def 3; :: thesis: verum[x,z] in [:X,Z:]

let x, z be object ; :: thesis: ( [x,z] in P * R implies [x,z] in [:X,Z:] )

assume [x,z] in P * R ; :: thesis: [x,z] in [:X,Z:]

then ex y being object st

( [x,y] in P & [y,z] in R ) by RELAT_1:def 8;

then ( x in X & z in Z ) by ZFMISC_1:87;

hence [x,z] in [:X,Z:] by ZFMISC_1:87; :: thesis: verum

end;assume [x,z] in P * R ; :: thesis: [x,z] in [:X,Z:]

then ex y being object st

( [x,y] in P & [y,z] in R ) by RELAT_1:def 8;

then ( x in X & z in Z ) by ZFMISC_1:87;

hence [x,z] in [:X,Z:] by ZFMISC_1:87; :: thesis: verum