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