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