1 / 2 < 0 + 1 ;
then not 1 / 2 is integer by INT_1:7;
hence not for b₁ being Real holds b₁ is integer ; :: thesis: verum