( 2 * 1 is heavy & 2 * 1 is even ) ;
hence ex b₁ being even Integer st b₁ is heavy ; :: thesis: verum