let I1, I2 be non empty closed_interval Subset of REAL; ( upper_bound I1 = lower_bound I2 implies ex a, b, c being Real st
( a <= c & c <= b & I1 = [.a,c.] & I2 = [.c,b.] ) )
assume A1:
upper_bound I1 = lower_bound I2
; ex a, b, c being Real st
( a <= c & c <= b & I1 = [.a,c.] & I2 = [.c,b.] )
consider a1, b1 being Real such that
A2:
a1 <= b1
and
A3:
I1 = [.a1,b1.]
by Th33;
consider a2, b2 being Real such that
A4:
a2 <= b2
and
A5:
I2 = [.a2,b2.]
by Th33;
A6:
upper_bound I1 = b1
by A2, A3, JORDAN5A:19;
lower_bound I2 = a2
by A4, A5, JORDAN5A:19;
hence
ex a, b, c being Real st
( a <= c & c <= b & I1 = [.a,c.] & I2 = [.c,b.] )
by A1, A2, A4, A3, A5, A6; verum