1 <> 0 ;
hence not for b₁ being Rational holds b₁ is zero ; :: thesis: verum