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