theorem :: XXREAL_0:4

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