A1: A is permutation of A by Th38;
( A is empty implies A is ascending ) ;
hence ex b₁ being permutation of A st b₁ is ascending by A1, Th86; :: thesis: verum