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