2 divides 2 ;
hence ex b₁ being Prime st b₁ is even by INT_2:28; :: thesis: verum