let R be empty array of O; :: thesis: R is ascending
let a be ordinal number ; :: according to EXCHSORT:def 10 :: thesis: for b being ordinal number st a in dom R & b in dom R & a in b holds
R /. a <= R /. b
thus for b being ordinal number st a in dom R & b in dom R & a in b holds
R /. a <= R /. b ; :: thesis: verum