let C be non empty connected compact Subset of R^1 ; :: thesis: ex a, b being real number st
( a <= b & C = [.a,b.] )
reconsider C' = C as closed-interval Subset of REAL by Th112;
A1: inf C' <= sup C' by BORSUK_4:53;
A2: C' = [.(inf C'),(sup C').] by INTEGRA1:5;
then A3: sup C' in C by A1, XXREAL_1:1;
inf C' in C by A2, A1, XXREAL_1:1;
then reconsider p1 = inf C', p2 = sup C' as Point of R^1 by A3;
take p1 ; :: thesis: ex b being real number st
( p1 <= b & C = [.p1,b.] )
take p2 ; :: thesis: ( p1 <= p2 & C = [.p1,p2.] )
thus p1 <= p2 by BORSUK_4:53; :: thesis: C = [.p1,p2.]
thus C = [.p1,p2.] by INTEGRA1:5; :: thesis: verum