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