2 * 2 is even ;
hence ex b₁ being square Nat st b₁ is even ; :: thesis: verum