let a, b, c, d be ext-real number ; :: 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, Def9; :: thesis: verum