theorem :: EXCHSORT:77

for O being non empty connected Poset
for R being array of O
for C being 0 -based arr_computation of R st R is finite array of O & ( for a being Ordinal st inversions (C . a) <> {} holds
succ a in dom C ) holds
C is complete