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: lower_bound C9 <= upper_bound C9 by BORSUK_4:53;
A2: C9 = [.(lower_bound C9),(upper_bound C9).] by INTEGRA1:5;
then A3: upper_bound C9 in C by A1, XXREAL_1:1;
lower_bound C9 in C by A2, A1, XXREAL_1:1;
then reconsider p1 = lower_bound C9, p2 = upper_bound 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