1 is trivial ;
hence ex b₁ being Nat st b₁ is trivial ; :: thesis: verum