let a, b, c, d be ext-real number ; :: thesis: ( a <= b & c <= d implies max a,c <= max b,d )
A1: ( b <= max b,d & d <= max b,d ) by Th25;
assume ( a <= b & c <= d ) ; :: thesis: max a,c <= max b,d
then ( a <= max b,d & c <= max b,d ) by A1, Th2;
hence max a,c <= max b,d by Def9; :: thesis: verum