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