defpred S₁[ set , set ] means ex z being set st
( [$1,z] in P & [z,$2] in R );
consider Q being Relation such that
A1: for x, y being set holds
( [x,y] in Q iff ( x in dom P & y in 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 z being set st
( [x,z] in P & [z,y] in R ) )
let x, y be set ; :: thesis: ( [x,y] in Q iff ex z being set st
( [x,z] in P & [z,y] in R ) )
thus ( [x,y] in Q implies ex z being set st
( [x,z] in P & [z,y] in R ) ) by A1; :: thesis: ( ex z being set st
( [x,z] in P & [z,y] in R ) implies [x,y] in Q )
given z being set such that A2: ( [x,z] in P & [z,y] in R ) ; :: thesis: [x,y] in Q
( x in dom P & y in rng R ) by A2, Def4, Def5;
hence [x,y] in Q by A1, A2; :: thesis: verum