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