theorem Th313: :: XXREAL_1:313

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