A1: 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;

reconsider Q = [:X,Z:] as Relation ;
P * R c= Q by A1, RELAT_1:def 3;
hence P * R is Relation of X,Z by Def1; :: thesis: verum