:: deftheorem Def1 defines Equal_Div_interval DIOPHAN1:def 1 :
for t being 1 _greater Nat
for b₂ being SetSequence of REAL holds
( b₂ = Equal_Div_interval t iff for n being Nat holds b₂ . n = [.(n / t),((n / t) + (t ")).[ );