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