let a be ExtReal; :: thesis: ( a in REAL implies +infty > a )
assume a in REAL ; :: thesis: +infty > a
then A1: a <> +infty by Lm0;
+infty >= a by Def5, Lm3, Lm5;
hence +infty > a by A1, Th1; :: thesis: verum