2 * (- 1) is heavy by COMPLEX3:1;
hence ex b₁ being negative Integer st b₁ is heavy ; :: thesis: verum