theorem Th318: :: XXREAL_1:318

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