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

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

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

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

end;

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

then A4: max (a,b) >= max (b,c) by Th26;
min (a,b) >= min (b,c) by A3, Th18;
hence max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = max ((min (a,b)),(min (c,a))) by Def9
.= max ((min (a,b)),c) by A3, Def8
.= min ((max (c,b)),a) by A3, Th37
.= min ((max (c,b)),(max (c,a))) by A3, Def9
.= min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) by A4, Def8 ;
:: thesis: verum

end;

end;