let r, q, p be ext-real number ; :: 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