let a, b, c, d be ExtReal; ( a < b & c < d implies min (a,c) < min (b,d) )
assume that
A1:
a < b
and
A2:
c < d
; min (a,c) < min (b,d)
min (a,c) <= c
by Th17;
then A3:
min (a,c) < d
by A2, Th2;
min (a,c) <= a
by Th17;
then
min (a,c) < b
by A1, Th2;
hence
min (a,c) < min (b,d)
by A3, Def8; verum