let a, c, b, d be real number ; :: thesis: ( 0 < a & 0 < c & a <= b & c < d implies a * c < b * d )
assume A1: ( 0 < a & 0 < c & a <= b & c < d ) ; :: thesis: a * c < b * d
then A2: a * c < a * d by Lm13;
a * d <= b * d by A1, Lm12;
hence a * c < b * d by A2, XXREAL_0:2; :: thesis: verum