theorem Th316: :: XXREAL_1:316

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