let a, b, c be ext-real number ; :: thesis: max a,(min b,c) = min (max a,b),(max a,c)

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

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

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

end;

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

then A4: max a,c <= max a,b by Th26;
thus max a,(min b,c) = max a,c by A3, Def8
.= min (max a,b),(max a,c) by A4, Def8 ; :: thesis: verum

end;

end;