theorem Lm7: :: DIOPHAN1:31

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 in (Equal_Div_interval t) . i )