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:43;
set S = [.p1,p2.];
reconsider S = [.p1,p2.] as Subset of I[01] by BORSUK_1:40, 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:20;
A4: S is closed by Th20;
0 <= p1 by BORSUK_1:43;
then I[01] | S = Closed-Interval-TSpace (p1,p2) by A2, A1, TOPMETR:24;
hence [.p1,p2.] is non empty connected compact Subset of I[01] by A4, A3, COMPTS_1:8, CONNSP_1:def 3; :: thesis: verum