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