:: deftheorem defines divide_into_equal INTEGRA4:def 1 :
for A being non empty closed_interval Subset of REAL
for IT being Division of A
for n being Nat holds
( IT divide_into_equal n iff ( len IT = n & ( for i being Nat st i in dom IT holds
IT . i = (lower_bound A) + (((vol A) / (len IT)) * i) ) ) );