n + 1 >= n + 0 by XREAL_1:6;
hence for b₁ being Nat st b₁ is n + 1 _or_greater holds
b₁ is n _or_greater by XXREAL_0:2; :: thesis: verum