let a, b, c be ExtReal; max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
per cases
( b <= c or c <= b )
;
suppose A1:
b <= c
;
max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))then A2:
max (
a,
b)
<= max (
a,
c)
by Th26;
thus max (
a,
(min (b,c))) =
max (
a,
b)
by A1, Def8
.=
min (
(max (a,b)),
(max (a,c)))
by A2, Def8
;
verum end; suppose A3:
c <= b
;
max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))then A4:
max (
a,
c)
<= max (
a,
b)
by Th26;
thus max (
a,
(min (b,c))) =
max (
a,
c)
by A3, Def8
.=
min (
(max (a,b)),
(max (a,c)))
by A4, Def8
;
verum end; end;