let C be non empty connected compact Subset of I[01]; :: thesis: C is non empty closed_interval Subset of REAL
reconsider C9 = C as Subset of REAL by BORSUK_1:40, XBOOLE_1:1;
( C9 is bounded_below & C9 is bounded_above ) by Th22;
then A1: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
A2: C9 is closed by Th24;
then A3: upper_bound C9 in C9 by Th22, RCOMP_1:12;
lower_bound C9 in C9 by A2, Th22, RCOMP_1:13;
then [.(lower_bound C9),(upper_bound C9).] = C9 by A3, Th19, Th26;
hence C is non empty closed_interval Subset of REAL by A1, MEASURE5:14; :: thesis: verum