let p, q be ext-real number ; :: thesis: ( p <= q implies p in [.-infty,q.] )
p >= -infty by XXREAL_0:5;
hence ( p <= q implies p in [.-infty,q.] ) by Th1; :: thesis: verum