theorem :: XXREAL_1:252

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