theorem Th81: :: XREAL_1:81

for a, b, c being Real st 0 < b & a * b < c holds
a < c / b