:: deftheorem defines delta INTEGRA3:def 1 :
for A being non empty closed_interval Subset of REAL
for D being Division of A holds delta D = max (rng (upper_volume ((chi (A,A)),D)));