:: 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 Element of NAT holds b₂ . n = halfline_fin ((n * (t ")),((n * (t ")) + (t "))) );