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