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