theorem :: XXREAL_1:140

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