let a, b, c be ExtReal; :: 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;