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