for p, q, r, s being ExtReal holds ].r,s.] \/ ].p,q.] c= ].(min (r,p)),(max (s,q)).]