theorem :: XXREAL_1:220

for p, q being ExtReal st p <= q holds
p in [.-infty,q.]