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