theorem Th314: :: XXREAL_1:314

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