let p, q, r be ExtReal; :: thesis: ( r <= p & p <= q implies [.r,q.[ \ {p} = [.r,p.[ \/ ].p,q.[ )
[.p,p.] = {p} by Th17;
hence ( r <= p & p <= q implies [.r,q.[ \ {p} = [.r,p.[ \/ ].p,q.[ ) by Th310; :: thesis: verum