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