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