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;

end;

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;max (a,b) = b by A1, Def9;

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