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