defpred S₁[ set , set ] means ex p, s, q, t being set 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 set 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 set holds
( [x,y] in Q iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
let x, y be set ; :: thesis: ( [x,y] in Q iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )

hereby :: thesis: ( ex p, q, s, t being set 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 set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
then consider p, s, q, t being set 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 set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
take q = q; :: thesis: ex s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
take s = s; :: thesis: ex t being set 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 set such that A3: ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ; :: thesis: [x,y] in Q
( p in dom P & q in dom R & s in rng P & t in rng R ) by A3, RELAT_1:20;
then ( x in [:(dom P),(dom R):] & y in [:(rng P),(rng R):] ) by A3, ZFMISC_1:106;
hence [x,y] in Q by A1, A3; :: thesis: verum