theorem Th86: :: EXCHSORT:86

for O being non empty connected Poset
for A being non empty finite 0 -based array of O ex B being permutation of A st B is ascending