for I being non empty closed_interval Subset of REAL
for r being Real st I = {r} holds
for D being Division of I holds D = <*r*>