theorem Th58: :: XXREAL_1:58
for p, q, r, s being ExtReal st r <= s & [.r,s.] c= ].p,q.] holds
( p < r & s <= q )