let E be Subset of I(01) ; :: thesis: ( 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 & E = [.p1,p2.] ) ; :: thesis: I[01] ,I(01) | E are_homeomorphic
reconsider T = I(01) | E as SubSpace of I[01] by TSEP_1:7;
( 0 <= p1 & p2 <= 1 ) by BORSUK_1:86;
then reconsider S = Closed-Interval-TSpace p1,p2 as SubSpace of I[01] by A1, TOPMETR:27, TREAL_1:6;
the carrier of S = E by A1, TOPMETR:25;
then A2: 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 A2, TOPMETR:27, T_0TOPSP:def 1; :: thesis: verum