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