theorem :: XXREAL_1:268

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