let p1, p2 be Point of I[01] ; :: thesis: ( p1 <= p2 implies [.p1,p2.] is non empty connected compact Subset of I[01] )
A1: 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;
assume A2: p1 <= p2 ; :: thesis: [.p1,p2.] is non empty connected compact Subset of I[01]
then A3: Closed-Interval-TSpace p1,p2 is connected by TREAL_1:23;
A4: S is closed by Th48;
0 <= p1 by BORSUK_1:86;
then I[01] | S = Closed-Interval-TSpace p1,p2 by A2, A1, TOPMETR:31;
hence [.p1,p2.] is non empty connected compact Subset of I[01] by A4, A3, COMPTS_1:17, CONNSP_1:def 3; :: thesis: verum