theorem :: XXREAL_0:6

for a being ExtReal st -infty >= a holds
a = -infty by Lm8;