2 * 0 is weightless ;
hence ex b₁ being even Integer st b₁ is weightless ; :: thesis: verum