let a, b, c, d be ext-real number ; :: thesis: ( a < b & c < d implies min a,c < min b,d )
A1: ( min a,c <= a & min a,c <= c ) by Th17;
assume ( a < b & c < d ) ; :: thesis: min a,c < min b,d
then ( min a,c < b & min a,c < d ) by A1, Th2;
hence min a,c < min b,d by Def8; :: thesis: verum