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