for x being Real
for A being non empty closed_interval Subset of REAL
for D being Division of A st x in A holds
ex j being Element of NAT st
( j in dom D & x in divset (D,j) )