let a, b, c be ExtReal; :: thesis: max ((max (a,b)),c) = max (a,(max (b,c)))

per cases ( ( a <= b & a <= c ) or ( b <= a & b <= c ) or ( c <= b & c <= a ) ) by Th2;

suppose A1: ( a <= b & a <= c ) ; :: thesis: max ((max (a,b)),c) = max (a,(max (b,c)))

A2: ( max (b,c) = b or max (b,c) = c ) by Def9;
max (a,b) = b by A1, Def9;
hence max ((max (a,b)),c) = max (a,(max (b,c))) by A1, A2, Def9; :: thesis: verum

end;

suppose A3: ( b <= a & b <= c ) ; :: thesis: max ((max (a,b)),c) = max (a,(max (b,c)))

then max (a,b) = a by Def9;
hence max ((max (a,b)),c) = max (a,(max (b,c))) by A3, Def9; :: thesis: verum

end;

suppose A4: ( c <= b & c <= a ) ; :: thesis: max ((max (a,b)),c) = max (a,(max (b,c)))

A5: ( max (a,b) = b or max (a,b) = a ) by Def9;
max (b,c) = b by A4, Def9;
hence max ((max (a,b)),c) = max (a,(max (b,c))) by A4, A5, Def9; :: thesis: verum

end;

end;