let a, b, c be ExtReal; :: thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))

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

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

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

end;

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

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

end;

end;