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