let a, b, c be ext-real number ; :: 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 Def10;
max a,b = b by A1, Def10;
hence max (max a,b),c = max a,(max b,c) by A1, A2, Def10; :: 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 Def10;
hence max (max a,b),c = max a,(max b,c) by A3, Def10; :: 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 Def10;
max b,c = b by A4, Def10;
hence max (max a,b),c = max a,(max b,c) by A4, A5, Def10; :: thesis: verum

end;

end;