let a, c, b be ext-real number ; :: 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, Def9;
hence max (a,(min (b,c))) = min (b,c) by Def10
.= min ((max (a,b)),c) by A2, Def10 ;
:: 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 Def9
.= a by A3, Def10
.= min (a,c) by A1, Def9
.= min ((max (a,b)),c) by A3, Def10 ;
:: thesis: verum

end;

end;