:: deftheorem defines decreasing ORDINAL5:def 1 :
for f being Sequence holds
( f is decreasing iff for a, b being Ordinal st a in b & b in dom f holds
f . b in f . a );