for t being 1 _greater Nat
for r being Real
for i being Nat st r in (Equal_Div_interval t) . i holds
[\(r * t)/] = i