defpred S₁[ Element of X, Element of X] means f . ($1,$2) <= a;
consider R being Relation of X,X such that
A1: for x, y being Element of X holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
take R ; :: thesis: for x, y being Element of X holds
( [x,y] in R iff f . (x,y) <= a )
thus for x, y being Element of X holds
( [x,y] in R iff f . (x,y) <= a ) by A1; :: thesis: verum