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