take r + 1 ; :: thesis: r + 1 is r _greater
r + 0 < r + 1 by XREAL_1:8;
hence r + 1 is r _greater ; :: thesis: verum