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