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