theorem Th07: :: BKMODEL3:6

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