r + 0 < r + s by XREAL_1:6;
hence not [.r,(r + s).] is empty by XXREAL_1:1; :: thesis: verum