let C be non empty connected compact Subset of I[01] ; :: thesis: C is closed-interval Subset of REAL
reconsider C' = C as Subset of REAL by BORSUK_1:83, XBOOLE_1:1;
A1: C' is closed by Th52;
A2: ( C' is bounded_below & C' is bounded_above ) by Th50;
then A3: inf C' in C' by A1, RCOMP_1:31;
sup C' in C' by A1, A2, RCOMP_1:30;
then A4: [.(inf C'),(sup C').] = C' by A3, Th47, Th54;
C' is bounded by A2;
then lower_bound C' <= upper_bound C' by SEQ_4:24;
hence C is closed-interval Subset of REAL by A4, INTEGRA1:def 1; :: thesis: verum