let p, q be ExtReal; :: thesis: ( q <= p implies p in [.q,+infty.] )
p <= +infty by XXREAL_0:3;
hence ( q <= p implies p in [.q,+infty.] ) by Th1; :: thesis: verum