(2 * 0) + 1 is odd ;
hence for b₁ being Nat st not b₁ is zero & b₁ is trivial holds
b₁ is odd by NAT_2:def 1; :: thesis: verum