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:86;
0 <= p1
by BORSUK_1:86;
then reconsider S = Closed-Interval-TSpace p1,p2 as SubSpace of I[01] by A1, A3, TOPMETR:27, TREAL_1:6;
reconsider T = I(01) | E as SubSpace of I[01] by TSEP_1:7;
the carrier of S = E
by A1, A2, TOPMETR:25;
then A4:
S = T
by PRE_TOPC:29, TSEP_1:5;
set f = L[01] ((#) p1,p2),(p1,p2 (#) );
L[01] ((#) p1,p2),(p1,p2 (#) ) is being_homeomorphism
by A1, TREAL_1:20;
hence
I[01] ,I(01) | E are_homeomorphic
by A4, TOPMETR:27, T_0TOPSP:def 1; verum