:: deftheorem Def12 defines less NOMIN_4:def 12 :
for A being set
for b₂ being Function of [:A,A:],BOOLEAN holds
( b₂ = less A iff 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 ) ) );