let C be non empty connected compact Subset of R^1; :: thesis: C is non empty closed_interval Subset of REAL
reconsider C9 = C as non empty Subset of REAL by TOPMETR:17;
C is closed by COMPTS_1:7;
then A1: C9 is closed by JORDAN5A:23;
then A2: upper_bound C9 in C9 by Th72, RCOMP_1:12;
( C9 is bounded_below & C9 is bounded_above ) by Th72;
then C9 is real-bounded by XXREAL_2:def 11;
then A3: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
lower_bound C9 in C9 by A1, Th72, RCOMP_1:13;
then [.(lower_bound C9),(upper_bound C9).] = C9 by A2, Th74, Th76;
then ( not C9 is empty & C9 is closed_interval ) by A3, MEASURE5:14;
hence C is non empty closed_interval Subset of REAL ; :: thesis: verum