defpred S₁[ object , object ] means $1 less_pred $2;
for f, g being Function of [:A,A:],BOOLEAN st ( 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 ) ) ) & ( for x, y being object st x in A & y in A holds
( ( S₁[x,y] implies g . (x,y) = TRUE ) & ( not S₁[x,y] implies g . (x,y) = FALSE ) ) ) holds
f = g from NOMIN_4:sch 2();
hence for b₁, b₂ being Function of [:A,A:],BOOLEAN st ( for x, y being object st x in A & y in A holds
( ( x less_pred y implies b₁ . (x,y) = TRUE ) & ( not x less_pred y implies b₁ . (x,y) = FALSE ) ) ) & ( for x, y being object st x in A & y in A holds
( ( x less_pred y implies b₂ . (x,y) = TRUE ) & ( not x less_pred y implies b₂ . (x,y) = FALSE ) ) ) holds
b₁ = b₂ ; :: thesis: verum