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 Lm12;
a * d < b * d by A1, Lm13;
hence a * c < b * d by A2, XXREAL_0:2; :: thesis: verum