:: deftheorem defines descending ORDERS_5:def 21 :
for A being RelStr
for s being FinSequence of A holds
( s is descending iff for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. m <~ s /. n );