theorem :: XXREAL_1:88

for r, s being ExtReal holds ].r,s.] misses {r}