theorem Lm9: :: DIOPHAN1:33

for t being 1 _greater Nat
for r being Real st r in [.0,1.[ holds
ex i being Nat st
( i <= t - 1 & [\(r * t)/] = i )