theorem :: XXREAL_1:246

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