theorem Th317: :: XXREAL_1:317

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