theorem :: XXREAL_0:38

for a, b, c being ExtReal holds min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))