let a, b be Real; :: thesis: ( a < 0 & a < b implies b / a < 1 )
assume that
A1: a < 0 and
A2: a < b ; :: thesis: b / a < 1
assume b / a >= 1 ; :: thesis: contradiction
then (b / a) * a <= 1 * a by A1, Lm28;
hence contradiction by A1, A2, XCMPLX_1:87; :: thesis: verum