( not 3 is trivial & (2 * 1) + 1 is odd ) ;
hence not for b₁ being odd Nat holds b₁ is trivial ; :: thesis: verum