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