theorem :: XXREAL_1:82

for p, q, r, s being ExtReal st r <= s & [.r,s.] c< [.p,q.] & not p < r holds
s < q