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