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