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