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