theorem Th83: :: XREAL_1:83

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