theorem :: XXREAL_1:278
for p, q, r, s being ExtReal st s < p holds
[.r,s.] misses [.p,q.]