now

let x, z be set ; :: 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 set 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;

hence P * R is Relation of X,Z by RELAT_1:def 3; :: thesis: verum