theorem Th319: :: XXREAL_1:319
for p, q, r being ExtReal st r < q & p <= q holds
].r,q.] \ [.p,q.[ = ].r,p.[ \/ {q}