( (2 * 1) + 1 is odd & 3 is prime ) by PEPIN:41;
hence ex b₁ being prime Nat st b₁ is odd ; :: thesis: verum