theorem Th26: :: BORSUK_4:29

for C being non empty connected compact Subset of I[01]
for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds
[.(lower_bound C9),(upper_bound C9).] = C9