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 ( a <= b & a <= c ) ; :: thesis: max (max a,b),c = max a,(max b,c)

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

end;

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

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

end;

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

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

end;

end;