( (2 * 0) + 1 is odd & 1 |^ 2 is square ) ;
hence ex b₁ being square Integer st b₁ is odd ; :: thesis: verum