theorem :: XXREAL_0:5

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