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