let a be ext-real number ; :: thesis: min (a,+infty) = a
a <= +infty by Def5, Lm2, Lm4;
hence min (a,+infty) = a by Def9; :: thesis: verum