defpred S₁[ object , object ] means ( $2 in Y & [$1,$2] in R );
consider P being Relation such that
A1: for x, y being object holds
( [x,y] in P iff ( x in dom R & y in rng R & S₁[x,y] ) ) from RELAT_1:sch 1();
take P ; :: thesis: for x, y being object holds
( [x,y] in P iff ( y in Y & [x,y] in R ) )
let x, y be object ; :: thesis: ( [x,y] in P iff ( y in Y & [x,y] in R ) )
( y in Y & [x,y] in R implies ( x in dom R & y in rng R ) ) by XTUPLE_0:def 12, XTUPLE_0:def 13;
hence ( [x,y] in P iff ( y in Y & [x,y] in R ) ) by A1; :: thesis: verum