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