theorem :: XXREAL_1:251

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