theorem Th320: :: XXREAL_1:320

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