2 is heavy ;
hence ex b₁ being positive Real st b₁ is heavy ; :: thesis: verum