let a be ext-real number ; :: thesis: max (a,-infty) = a
a >= -infty by Def5, Lm3, Lm5;
hence max (a,-infty) = a by Def10; :: thesis: verum