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

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