theorem :: XXREAL_0:3

for a being ExtReal holds a <= +infty by Def5, Lm3, Lm5;