for a being ExtReal st +infty <= a holds
a = +infty by Lm9;