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