let a be ext-real number ; :: thesis: ( a in REAL implies +infty > a )
A1: +infty >= a by Def5, Lm2, Lm4;
assume a in REAL ; :: thesis: +infty > a
then a <> +infty ;
hence +infty > a by A1, Th1; :: thesis: verum