theorem :: XXREAL_1:370

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