let E be Subset of I(01); ( ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) implies I[01] ,I(01) | E are_homeomorphic )
given p1, p2 being Point of I[01] such that A1:
p1 < p2
and
A2:
E = [.p1,p2.]
; I[01] ,I(01) | E are_homeomorphic
A3:
p2 <= 1
by BORSUK_1:43;
0 <= p1
by BORSUK_1:43;
then reconsider S = Closed-Interval-TSpace (p1,p2) as SubSpace of I[01] by A1, A3, TOPMETR:20, TREAL_1:3;
reconsider T = I(01) | E as SubSpace of I[01] by TSEP_1:7;
the carrier of S = E
by A1, A2, TOPMETR:18;
then A4:
S = T
by PRE_TOPC:8, TSEP_1:5;
set f = L[01] (((#) (p1,p2)),((p1,p2) (#)));
L[01] (((#) (p1,p2)),((p1,p2) (#))) is being_homeomorphism
by A1, TREAL_1:17;
hence
I[01] ,I(01) | E are_homeomorphic
by A4, TOPMETR:20, T_0TOPSP:def 1; verum