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