let a, b, c, d be Real; :: thesis: ( 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 ; :: thesis: a * c < b * d
A5: a * c < a * d by A1, A4, Lm24;
a * d <= b * d by A2, A3, A4, Lm28;
hence a * c < b * d by A5, XXREAL_0:2; :: thesis: verum