now for x, z being object st [x,z] in P * R holds
[x,z] in [:X,Z:]let x,
z be
object ;
( [x,z] in P * R implies [x,z] in [:X,Z:] )assume
[x,z] in P * R
;
[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;
verum end;
hence
P * R is Relation of X,Z
by RELAT_1:def 3; verum