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