for Iac, Icb being non empty closed_interval Subset of REAL
for Dac being Division of Iac
for Dcb being Division of Icb st upper_bound Iac = lower_bound Icb & len Dcb = 1 & Dcb . 1 = lower_bound Icb holds
Dac (#) Dcb = Dac