:: deftheorem defines descending EXCHSORT:def 8 :
for f being Function holds
( f is descending iff for a, b being Ordinal st a in dom f & b in dom f & a in b holds
f . b c< f . a );