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