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