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 C9 = C as closed-interval Subset of REAL by Th112;
A1: inf C9 <= sup C9 by BORSUK_4:53;
A2: C9 = [.(inf C9),(sup C9).] by INTEGRA1:5;
then A3: sup C9 in C by A1, XXREAL_1:1;
inf C9 in C by A2, A1, XXREAL_1:1;
then reconsider p1 = inf C9, p2 = sup C9 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