theorem :: XXREAL_1:200

for p, q, r, s being ExtReal st p <= r & s <= q holds
[.p,q.] \ ([.p,r.] \/ [.s,q.]) = ].r,s.[