theorem Th62: :: XXREAL_1:62

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