theorem :: XXREAL_1:265

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