theorem :: XXREAL_1:275

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