( 2 is even & 2 is prime ) by INT_2:28;
hence ex b₁ being prime Nat st b₁ is even ; :: thesis: verum