r - s < r - 0 by XREAL_1:15;
hence not ].(r - s),r.] is empty by XXREAL_1:32; :: thesis: verum