let a be ExtReal; :: thesis: max (a,-infty) = a
a >= -infty by Def5, Lm4, Lm6;
hence max (a,-infty) = a by Def9; :: thesis: verum