let a, b, c, d be real number ; :: thesis: ( a < 0 & b <= a & c < 0 & d < c implies a * c < b * d )
assume A1: ( 0 > a & a >= b & 0 > c & c > d ) ; :: thesis: a * c < b * d
then A2: a * c < a * d by Lm25;
a * d <= b * d by A1, Lm31;
hence a * c < b * d by A2, XXREAL_0:2; :: thesis: verum