for A being non empty closed_interval Subset of REAL
for D being Division of A
for t being Element of A st lower_bound A < D . 1 holds
ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )