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)

per cases ( a <= b or b <= a ) ;

suppose A2: a <= b ; :: thesis: max (a,(min (b,c))) = min ((max (a,b)),c)

then a <= min (b,c) by A1, Def8;
hence max (a,(min (b,c))) = min (b,c) by Def9
.= min ((max (a,b)),c) by A2, Def9 ;
:: thesis: verum

end;

suppose A3: b <= a ; :: thesis: max (a,(min (b,c))) = min ((max (a,b)),c)

then b <= c by A1, Th2;
hence max (a,(min (b,c))) = max (a,b) by Def8
.= a by A3, Def9
.= min (a,c) by A1, Def8
.= min ((max (a,b)),c) by A3, Def9 ;
:: thesis: verum

end;

end;