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