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