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