let I1, I2, I be non empty closed_interval Subset of REAL; :: thesis: ( upper_bound I1 <= lower_bound I2 & lower_bound I <= lower_bound I1 & upper_bound I2 <= upper_bound I implies I1 \/ I2 c= I )
assume that
A1: upper_bound I1 <= lower_bound I2 and
A2: lower_bound I <= lower_bound I1 and
A3: upper_bound I2 <= upper_bound I ; :: thesis: I1 \/ I2 c= I
consider a1, b1 being Real such that
A4: I1 = [.a1,b1.] by MEASURE5:def 3;
A5: a1 <= b1 by A4, XXREAL_1:29;
then A6: ( lower_bound I1 = a1 & upper_bound I1 = b1 ) by A4, JORDAN5A:19;
consider a2, b2 being Real such that
A7: I2 = [.a2,b2.] by MEASURE5:def 3;
A8: a2 <= b2 by A7, XXREAL_1:29;
A9: ( lower_bound I <= a1 & b2 <= upper_bound I ) by A2, A3, A5, A4, JORDAN5A:19, A8, A7;
A10: b1 <= a2 by A6, A1, A8, A7, JORDAN5A:19;
consider a3, b3 being Real such that
A11: I = [.a3,b3.] by MEASURE5:def 3;
a3 <= b3 by A11, XXREAL_1:29;
then A12: ( lower_bound I = a3 & upper_bound I = b3 ) by A11, JORDAN5A:19;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I1 \/ I2 or x in I )
assume A13: x in I1 \/ I2 ; :: thesis: x in I
then reconsider x1 = x as Real ;