theorem :: XXREAL_1:344

for p, q being ExtReal st p <= q holds
[.-infty,q.] \ [.p,q.[ = [.-infty,p.[ \/ {q}