for a being ExtReal holds a >= -infty by Def5, Lm4, Lm6;