theorem Th178: :: XXREAL_1:178
for p, q, r, s being ExtReal st p < s & r < q & s <= r holds
].p,r.] \/ [.s,q.[ = ].p,q.[