:: deftheorem Def1 defines EqDiv MESFUN14:def 1 :
for A being non empty closed_interval Subset of REAL
for n being Nat st n > 0 & vol A > 0 holds
for b₃ being Division of A holds
( b₃ = EqDiv (A,n) iff b₃ divide_into_equal n );