let p1, p2 be Point of I[01] ; :: thesis: ( p1 <= p2 implies [.p1,p2.] is non empty connected compact Subset of I[01] )
assume A1: p1 <= p2 ; :: thesis: [.p1,p2.] is non empty connected compact Subset of I[01]
A2: ( 0 <= p1 & p2 <= 1 ) by BORSUK_1:86;
set S = [.p1,p2.];
reconsider S = [.p1,p2.] as Subset of I[01] by BORSUK_1:83, XXREAL_2:def 12;
A3: S is closed by Th48;
A4: Closed-Interval-TSpace p1,p2 is connected by A1, TREAL_1:23;
I[01] | S = Closed-Interval-TSpace p1,p2 by A1, A2, TOPMETR:31;
hence [.p1,p2.] is non empty connected compact Subset of I[01] by A1, A3, A4, COMPTS_1:17, CONNSP_1:def 3, XXREAL_1:1; :: thesis: verum