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