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