theorem :: XXREAL_1:267

for q, s being ExtReal
for r being Real st s < q holds
[.r,s.] c= ].-infty,q.[