let a, b be real number ; :: thesis: ( a < 0 & b < a implies 1 < b / a )
assume A1: ( a < 0 & b < a ) ; :: thesis: 1 < b / a
then b / a > a / a by Lm32;
hence b / a > 1 by A1, XCMPLX_1:60; :: thesis: verum