theorem :: XXREAL_1:141

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