theorem :: XXREAL_1:425

for r being ExtReal holds [.r,+infty.] = [.r,+infty.[ \/ {+infty} by Th129, XXREAL_0:3;