reconsider a = 1 as rational number ;
a <> 0 ;
hence not for b₁ being rational number holds b₁ is empty ; :: thesis: verum