theorem :: XXREAL_0:40

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