let a, b, c be real number ; :: thesis: ( a <= b & c <= 0 implies b * c <= a * c )
assume A1: a <= b ; :: thesis: ( not c <= 0 or b * c <= a * c )
assume c <= 0 ; :: thesis: b * c <= a * c
then a * (- c) <= b * (- c) by A1, Lm12;
then - (a * c) <= - (b * c) ;
hence b * c <= a * c by Lm15; :: thesis: verum