1 is weightless ;
hence ex b₁ being weightless Integer st b₁ is positive ; :: thesis: verum