let p1, p2 be Point of I[01]; ( 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
; [.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; verum