theorem :: XXREAL_1:248

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