- 4 is heavy ;
hence ex b₁ being Integer st b₁ is heavy ; :: thesis: verum