let a, b, c, d be Real; ( a <= 0 & b <= a & c <= 0 & d <= c 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:
- c <= - d
by A4, Lm14;
- a <= - b
by A2, Lm14;
then
(- a) * (- c) <= (- b) * (- d)
by A1, A3, A5, Th66;
hence
a * c <= b * d
; verum