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: min a,b <= min b,c by Th18;
A3: max a,b <= max b,c by A1, Th26;
thus max (max (min a,b),(min b,c)),(min c,a) = max (min b,c),(min c,a) by A2, 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 A3, Def8 ; :: thesis: verum

end;

suppose A4: 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 A5: min a,b >= min b,c by Th18;
A6: max a,b >= max b,c by A4, Th26;
thus max (max (min a,b),(min b,c)),(min c,a) = max (min a,b),(min c,a) by A5, Def9
.= max (min a,b),c by A4, Def8
.= min (max c,b),a by A4, Th37
.= min (max c,b),(max c,a) by A4, Def9
.= min (min (max a,b),(max b,c)),(max c,a) by A6, Def8 ; :: thesis: verum

end;

end;