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