for p, q being ExtReal st p > q holds
p in ].q,+infty.] by XXREAL_0:3, Th2;