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