let a, b, c, d be Real; ( 0 <= a & a <= b & 0 <= c & c <= d implies a * c <= b * d )
assume that
A1:
0 <= a
and
A2:
a <= b
and
A3:
0 <= c
and
A4:
c <= d
; a * c <= b * d
A5:
a * c <= b * c
by A2, A3, Lm12;
b * c <= b * d
by A1, A2, A4, Lm12;
hence
a * c <= b * d
by A5, XXREAL_0:2; verum