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