s + r <= s - r by XREAL_1:8;
hence ].(s - r),(s + r).[ is empty by XXREAL_1:28; :: thesis: verum