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