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

end;

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

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