let b, a, c be real number ; :: thesis: ( 0 < b & a * b < c implies a < c / b )
assume A1: ( b > 0 & a * b < c ) ; :: thesis: a < c / b
then (a * b) / b < c / b by Lm28;
hence a < c / b by A1, XCMPLX_1:90; :: thesis: verum