let I1, I2, I be non empty closed_interval Subset of REAL; :: thesis: ( upper_bound I1 = lower_bound I2 & I = I1 \/ I2 implies ( lower_bound I = lower_bound I1 & upper_bound I = upper_bound I2 ) )
assume that
A1: upper_bound I1 = lower_bound I2 and
A2: I = I1 \/ I2 ; :: thesis: ( lower_bound I = lower_bound I1 & upper_bound I = upper_bound I2 )
A3: I1 = [.(lower_bound I1),(upper_bound I1).] by INTEGRA1:4;
then A4: lower_bound I1 <= upper_bound I1 by XXREAL_1:29;
A5: I2 = [.(lower_bound I2),(upper_bound I2).] by INTEGRA1:4;
then A6: lower_bound I2 <= upper_bound I2 by XXREAL_1:29;
A7: I = [.(lower_bound I1),(upper_bound I2).] by A2, A3, A5, A1, A4, A6, XXREAL_1:165;
A8: I = [.(lower_bound I),(upper_bound I).] by INTEGRA1:4;
then lower_bound I <= upper_bound I by XXREAL_1:29;
hence ( lower_bound I = lower_bound I1 & upper_bound I = upper_bound I2 ) by A7, A8, XXREAL_1:66; :: thesis: verum