theorem :: XXREAL_1:181

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