let a, b, c, d be ExtReal; ( a < b & c < d implies max (a,c) < max (b,d) )
assume that
A1:
a < b
and
A2:
c < d
; 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; verum