theorem :: XXREAL_1:176

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