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 Th311; :: thesis: verum