let a, b, c be ExtReal; :: thesis: ( a <= c implies max (a,(min (b,c))) = min ((max (a,b)),c) )

assume A1: a <= c ; :: thesis: max (a,(min (b,c))) = min ((max (a,b)),c)

assume A1: a <= c ; :: thesis: max (a,(min (b,c))) = min ((max (a,b)),c)