:: deftheorem defines -asc_ordering ORDERS_5:def 25 :
for A being RelStr
for B being Subset of A
for s being FinSequence of A holds
( s is B -asc_ordering iff ( s is asc_ordering & rng s = B ) );