let a, b, c, d be real number ; :: thesis: ( a <= 0 & b <= a & c <= 0 & d <= c implies a * c <= b * d )
assume ( 0 >= a & a >= b & 0 >= c & c >= d ) ; :: thesis: a * c <= b * d
then ( - 0 <= - a & - a <= - b & - 0 <= - c & - c <= - d ) by Lm14;
then ( (- a) * (- c) <= (- b) * (- d) & (- a) * (- c) <= (- d) * (- b) & (- c) * (- a) <= (- d) * (- b) & (- c) * (- a) <= (- b) * (- d) ) by Th68;
hence a * c <= b * d ; :: thesis: verum