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

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