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, 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;