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