let a,

b,

c be

ExtReal;

min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
per cases
( b <= c or c <= b )
;

suppose A1:
b <= c
;

min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))then A2:
min (

a,

b)

<= min (

a,

c)

by Th18;

thus min (

a,

(max (b,c))) =

min (

a,

c)

by A1, Def9
.=

max (

(min (a,b)),

(min (a,c)))

by A2, Def9
;

verum end; suppose A3:
c <= b
;

min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))then A4:
min (

a,

c)

<= min (

a,

b)

by Th18;

thus min (

a,

(max (b,c))) =

min (

a,

b)

by A3, Def9
.=

max (

(min (a,b)),

(min (a,c)))

by A4, Def9
;

verum end; end;