theorem :: XXREAL_1:279

for p, q, r, s being ExtReal st s < p holds
].r,s.] misses [.p,q.[