theorem Th08: :: BKMODEL3:7

for a, b being Real st 0 < a & 1 < b holds
(a / b) - a < 0