theorem Th1: :: EUCLID13:1

for i being Integer
for r being Real st 0 < i * r & i * r < r holds
i = 1