:: deftheorem Def1 defines c=-monotone KNASTER:def 1 :
for A, B being non empty set
for f being Function of A,B holds
( f is c=-monotone iff for x, y being Element of A st x c= y holds
f . x c= f . y );