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