theorem :: XXREAL_1:245

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