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