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