for p, r being ExtReal holds [.r,+infty.] \ ].p,+infty.[ = [.r,p.] \/ {+infty}