let a, b be Real; :: thesis: ( a < 0 & b < a implies 1 < b / a )
assume A1: a < 0 ; :: thesis: ( not b < a or 1 < b / a )
assume b < a ; :: thesis: 1 < b / a
then b / a > a / a by A1, Lm29;
hence 1 < b / a by A1, XCMPLX_1:60; :: thesis: verum