:: deftheorem Def12 defines non-increasing VALUED_0:def 16 :
for f being ext-real-valued Function holds
( f is non-increasing iff for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 >= f . e2 );