LexOrder n is admissible by Th22;
hence ex b₁ being TermOrder of n st b₁ is admissible ; :: thesis: verum