let a, b, c be ext-real number ; :: 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 Def10
.= max (min b,c),a by A1, Def9
.= min (max a,b),c by A1, Th37
.= min (max a,b),(max c,a) by A1, Def10
.= min (min (max a,b),(max b,c)),(max c,a) by A2, Def9 ;
:: 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 Def10
.= max (min a,b),c by A3, Def9
.= min (max c,b),a by A3, Th37
.= min (max c,b),(max c,a) by A3, Def10
.= min (min (max a,b),(max b,c)),(max c,a) by A4, Def9 ;
:: thesis: verum

end;

end;