theorem :: XXREAL_1:242

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