r + 0 < r + s by XREAL_1:6;
then ( r < (r + (r + s)) / 2 & (r + (r + s)) / 2 < r + s ) by XREAL_1:226;
hence not ].r,(r + s).[ is empty by XXREAL_1:4; :: thesis: verum