defpred S1[ object , object ] means ( A <- (f . $1) <> 0 & ( A <- (f . $1) < A <- (f . $2) or A <- (f . $2) = 0 ) );
consider R being Relation such that
A1:
for x, y being object holds
( [x,y] in R iff ( x in X & y in X & S1[x,y] ) )
from RELAT_1:sch 1();
R c= [:X,X:]
then reconsider R = R as Relation of X ;
take
R
; for x, y being set holds
( x,y in R iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) )
let x, y be set ; ( x,y in R iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) )
thus
( x,y in R iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) )
by A1; verum