:: deftheorem defines complete EXCHSORT:def 15 :
for O being non empty connected Poset
for R being array of O
for C being arr_computation of R holds
( C is complete iff last C is ascending );