theorem :: XXREAL_1:372

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