let q, p be ext-real number ; :: 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