let C be non empty connected compact Subset of R^1; :: thesis: ex a, b being Real st
( a <= b & C = [.a,b.] )
reconsider C9 = C as non empty closed_interval Subset of REAL by Th77;
A1: lower_bound C9 <= upper_bound C9 by BORSUK_4:28;
A2: C9 = [.(lower_bound C9),(upper_bound C9).] by INTEGRA1:4;
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 st
( p1 <= b & C = [.p1,b.] )
take p2 ; :: thesis: ( p1 <= p2 & C = [.p1,p2.] )
thus p1 <= p2 by BORSUK_4:28; :: thesis: C = [.p1,p2.]
thus C = [.p1,p2.] by INTEGRA1:4; :: thesis: verum