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