let a, b be Real; :: thesis: ( a <= 0 & b < a implies a / b < 1 )
assume A1: ( a <= 0 & b < a ) ; :: thesis: a / b < 1
then a / b < b / b by Lm29;
hence a / b < 1 by A1, XCMPLX_1:60; :: thesis: verum