let C be non empty connected compact Subset of R^1 ; :: thesis: C is non empty closed-interval Subset of REAL
reconsider C' = C as non empty Subset of REAL by TOPMETR:24;
C is closed by COMPTS_1:16;
then A1: C' is closed by TOPREAL6:79;
then A2: sup C' in C' by Th107, RCOMP_1:30;
( C' is bounded_below & C' is bounded_above ) by Th107;
then C' is bounded by XXREAL_2:def 11;
then A3: lower_bound C' <= upper_bound C' by SEQ_4:24;
inf C' in C' by A1, Th107, RCOMP_1:31;
then [.(inf C'),(sup C').] = C' by A2, Th109, Th111;
hence C is non empty closed-interval Subset of REAL by A3, INTEGRA1:def 1; :: thesis: verum