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