for I1, I2, I being non empty closed_interval Subset of REAL
for D1 being Division of I1
for D2 being Division of I2 st upper_bound I1 <= lower_bound I2 & I = [.(lower_bound I1),(upper_bound I2).] holds
D1 (#) D2 is Division of I