let a, b, c be Real; :: thesis: ( 0 < b & a * b < c implies a < c / b )
assume that
A1: b > 0 and
A2: a * b < c ; :: thesis: a < c / b
(a * b) / b < c / b by A1, A2, Lm26;
hence a < c / b by A1, XCMPLX_1:89; :: thesis: verum