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