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 consider y being set such that
A2: ( [x,y] in P & [y,z] in R ) by RELAT_1:def 8;
( x in X & z in Z ) by A2, ZFMISC_1:106;
hence [x,z] in [:X,Z:] by ZFMISC_1:106; :: thesis: verum

end;

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