theorem :: COUSIN:38

for I1, I2 being non empty closed_interval Subset of REAL st upper_bound I1 = lower_bound I2 holds
ex a, b, c being Real st
( a <= c & c <= b & I1 = [.a,c.] & I2 = [.c,b.] )