theorem :: XXREAL_1:177

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