defpred S₁[ object , object ] means ex p, s, q, t being object st
( $1 = [p,q] & $2 = [s,t] & [p,s] in P & [q,t] in R );
consider Q being Relation such that
A1: for x, y being object holds
( [x,y] in Q iff ( x in [:(dom P),(dom R):] & y in [:(rng P),(rng R):] & S₁[x,y] ) ) from RELAT_1:sch 1();
take Q ; :: thesis: for x, y being object holds
( [x,y] in Q iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
let x, y be object ; :: thesis: ( [x,y] in Q iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )

hereby :: thesis: ( ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) implies [x,y] in Q )

assume [x,y] in Q ; :: thesis: ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
then consider p, s, q, t being object such that
A2: ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) by A1;
take p = p; :: thesis: ex q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
take q = q; :: thesis: ex s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
take s = s; :: thesis: ex t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
take t = t; :: thesis: ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
thus ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) by A2; :: thesis: verum

end;

given p, q, s, t being object such that A3: x = [p,q] and
A4: y = [s,t] and
A5: ( [p,s] in P & [q,t] in R ) ; :: thesis: [x,y] in Q
( s in rng P & t in rng R ) by A5, XTUPLE_0:def 13;
then A6: y in [:(rng P),(rng R):] by A4, ZFMISC_1:87;
( p in dom P & q in dom R ) by A5, XTUPLE_0:def 12;
then x in [:(dom P),(dom R):] by A3, ZFMISC_1:87;
hence [x,y] in Q by A1, A3, A4, A5, A6; :: thesis: verum