defpred S₁[ 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 & 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 & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) )
let x, y be set ; :: thesis: ( 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; :: thesis: verum