:: deftheorem defines non-ascending PROB_1:def 4 :
for f being Function holds
( f is non-ascending iff for n, m being Nat st n <= m holds
f . m c= f . n );