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