let b, a be real number ; :: thesis: ( 0 < b & - 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, Lm12;
hence contradiction by A1, A2, XCMPLX_1:87; :: thesis: verum