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;