let C be non empty connected compact Subset of R^1; 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
; ex b being Real st
( p1 <= b & C = [.p1,b.] )
take
p2
; ( p1 <= p2 & C = [.p1,p2.] )
thus
p1 <= p2
by BORSUK_4:28; C = [.p1,p2.]
thus
C = [.p1,p2.]
by INTEGRA1:4; verum