:: deftheorem defines asc_ordering ORDERS_5:def 23 :
for A being RelStr
for s being FinSequence of A holds
( s is asc_ordering iff ( s is one-to-one & s is weakly-ascending ) );