defpred S₁[ object , object ] means ex z being object st
( [$1,z] in P & [z,$2] in R );
consider Q being Relation such that
A1: for x, y being object holds
( [x,y] in Q iff ( x in proj1 P & y in proj2 R & S₁[x,y] ) ) from RELAT_1:sch 1();
take Q ; :: thesis: for x, y being object holds
( [x,y] in Q iff ex z being object st
( [x,z] in P & [z,y] in R ) )
let x, y be object ; :: thesis: ( [x,y] in Q iff ex z being object st
( [x,z] in P & [z,y] in R ) )
thus ( [x,y] in Q implies ex z being object st
( [x,z] in P & [z,y] in R ) ) by A1; :: thesis: ( ex z being object st
( [x,z] in P & [z,y] in R ) implies [x,y] in Q )
given z being object such that A2: ( [x,z] in P & [z,y] in R ) ; :: thesis: [x,y] in Q
( x in proj1 P & y in proj2 R ) by A2, XTUPLE_0:def 12, XTUPLE_0:def 13;
hence [x,y] in Q by A1, A2; :: thesis: verum