let a, b, c, d be ExtReal; :: 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, Def9; :: thesis: verum