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 C' = C as closed-interval Subset of REAL by Th55;
A1: C' = [.(inf C'),(sup C').] by INTEGRA1:5;
A2: inf C' <= sup C' by Th53;
then A3: sup C' in C by A1, XXREAL_1:1;
inf C' in C by A1, A2, XXREAL_1:1;
then reconsider p1 = inf C', p2 = sup C' 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 Th53; :: thesis: C = [.p1,p2.]
thus C = [.p1,p2.] by INTEGRA1:5; :: thesis: verum