theorem :: XXREAL_1:180

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