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