theorem Lm5: :: DIOPHAN1:29

for i being Nat
for r1, r2 being Real
for t being 1 _greater Nat st r1 in (Equal_Div_interval t) . i & r2 in (Equal_Div_interval t) . i holds
|.(r1 - r2).| < t "