let a, b, c be ExtReal; 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
;
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
;
verum end; suppose A3:
c <= a
;
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
;
verum end; end;