let I1, I2, I be non empty closed_interval Subset of REAL; ( 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
; 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 ; TARSKI:def 3 ( not x in I1 \/ I2 or x in I )
assume A13:
x in I1 \/ I2
; x in I
then reconsider x1 = x as Real ;