theorem :: XXREAL_1:371

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