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