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