let C be non empty connected compact Subset of I[01]; :: thesis: ex p1, p2 being Point of I[01] st
( p1 <= p2 & C = [.p1,p2.] )
reconsider C9 = C as non empty closed_interval Subset of REAL by Th27;
A1: C9 = [.(lower_bound C9),(upper_bound C9).] by INTEGRA1:4;
A2: lower_bound C9 <= upper_bound C9 by Th25;
then A3: upper_bound C9 in C by A1, XXREAL_1:1;
lower_bound C9 in C by A1, A2, XXREAL_1:1;
then reconsider p1 = lower_bound C9, p2 = upper_bound C9 as Point of I[01] by A3;
take p1 ; :: thesis: ex p2 being Point of I[01] st
( p1 <= p2 & C = [.p1,p2.] )
take p2 ; :: thesis: ( p1 <= p2 & C = [.p1,p2.] )
thus p1 <= p2 by Th25; :: thesis: C = [.p1,p2.]
thus C = [.p1,p2.] by INTEGRA1:4; :: thesis: verum