let a be ExtReal; :: thesis: min (a,+infty) = a
a <= +infty by Def5, Lm3, Lm5;
hence min (a,+infty) = a by Def8; :: thesis: verum