defpred S_{1}[ 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_{1}[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

consider R being Relation of X,X such that

A1: for x, y being Element of X holds

( [x,y] in R iff S

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