let a, b, c be ext-real number ; :: thesis: min a,(max b,c) = max (min a,b),(min a,c)

per cases ( b <= c or c <= b ) ;

suppose A1: b <= c ; :: thesis: 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 ; :: thesis: verum

end;

suppose A3: c <= b ; :: thesis: 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 ; :: thesis: verum

end;

end;