theorem :: XXREAL_1:264
for q, r, s being ExtReal st s < q holds
].r,s.] c= ].-infty,q.[ by Th49, XXREAL_0:5;