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