:: deftheorem Def11 defines c=-monotone COHSP_1:def 11 :
for f being Function holds
( f is c=-monotone iff for a, b being set st a in dom f & b in dom f & a c= b holds
f . a c= f . b );