theorem :: XXREAL_1:164

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