theorem :: XXREAL_1:219

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