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