let p, q be ExtReal; :: 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