let O be non empty connected Poset; :: thesis: for A being non empty finite 0 -based array of O ex B being permutation of A st B is ascending
let A be non empty finite 0 -based array of O; :: thesis: ex B being permutation of A st B is ascending
consider C being 0 -based arr_computation of A such that
A1: C is complete by Th85;
C is finite by Th76;
then reconsider B = last C as permutation of A by Th78;
take B ; :: thesis: B is ascending
thus B is ascending by A1; :: thesis: verum