theorem :: XXREAL_1:179

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.]