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