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