let p, q, r, s be ExtReal; :: thesis: ( p <= r & s <= q implies [.p,q.] \ ([.p,r.] \/ [.s,q.]) = ].r,s.[ )
assume that
A1: p <= r and
A2: s <= q ; :: thesis: [.p,q.] \ ([.p,r.] \/ [.s,q.]) = ].r,s.[
thus [.p,q.] \ ([.p,r.] \/ [.s,q.]) = ([.p,q.] \ [.p,r.]) \ [.s,q.] by XBOOLE_1:41
.= ].r,q.] \ [.s,q.] by A1, Th182
.= ].r,s.[ by A2, Th191 ; :: thesis: verum