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