let a be ExtReal; :: thesis: max (a,+infty) = +infty
a <= +infty by Def5, Lm3, Lm5;
hence max (a,+infty) = +infty by Def9; :: thesis: verum