theorem :: XXREAL_1:249

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