defpred S₁[ object , object ] means f . $1 < f . $2;
consider R being Relation such that
A1: for x, y being object holds
( [x,y] in R iff ( x in X & y in X & S₁[x,y] ) ) from RELAT_1:sch 1();
R c= [:X,X:]

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R or [x,y] in [:X,X:] )
assume [x,y] in R ; :: thesis: [x,y] in [:X,X:]
then ( x in X & y in X ) by A1;
hence [x,y] in [:X,X:] by ZFMISC_1:87; :: thesis: verum

end;

then reconsider R = R as Relation of X ;
take R ; :: thesis: for x, y being set holds
( x,y in R iff ( x in X & y in X & f . x < f . y ) )
let x, y be set ; :: thesis: ( x,y in R iff ( x in X & y in X & f . x < f . y ) )
thus ( x,y in R iff ( x in X & y in X & f . x < f . y ) ) by A1; :: thesis: verum