for I1, I2, I being non empty closed_interval Subset of REAL st upper_bound I1 = lower_bound I2 & I = I1 \/ I2 holds
( lower_bound I = lower_bound I1 & upper_bound I = upper_bound I2 )