let a be ext-real number ; :: thesis: max (a,+infty) = +infty
a <= +infty by Def5, Lm2, Lm4;
hence max (a,+infty) = +infty by Def10; :: thesis: verum