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