:: deftheorem defines ascending EXCHSORT:def 10 :
for O being RelStr
for A being array of O holds
( A is ascending iff for a, b being Ordinal st a in dom A & b in dom A & a in b holds
A /. a <= A /. b );