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