theorem Th175: :: XXREAL_1:175

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