theorem :: XXREAL_1:237
for p, r, s being ExtReal st p <= r holds
[.r,s.] c= [.p,+infty.]