defpred S₁[ object , object ] means $1 less_pred $2;
consider f being Function of [:A,A:],BOOLEAN such that
A1: for x, y being object st x in A & y in A holds
( ( S₁[x,y] implies f . (x,y) = TRUE ) & ( not S₁[x,y] implies f . (x,y) = FALSE ) ) from NOMIN_4:sch 1();
take f ; :: thesis: for x, y being object st x in A & y in A holds
( ( x less_pred y implies f . (x,y) = TRUE ) & ( not x less_pred y implies f . (x,y) = FALSE ) )
thus for x, y being object st x in A & y in A holds
( ( x less_pred y implies f . (x,y) = TRUE ) & ( not x less_pred y implies f . (x,y) = FALSE ) ) by A1; :: thesis: verum