2 * 1 is heavy ;
hence ex b₁ being positive Integer st b₁ is heavy ; :: thesis: verum