for p, r, s being ExtReal st p < r holds
[.r,s.] c= ].p,+infty.] by Th39, XXREAL_0:3;