let Dp be non empty Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | Dp),I(01)
for C being non empty Subset of (TOP-REAL 2) st f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
let f be Function of ((TOP-REAL 2) | Dp),I(01) ; :: thesis: for C being non empty Subset of (TOP-REAL 2) st f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
let C be non empty Subset of (TOP-REAL 2); :: thesis: ( f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) implies ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 )
assume A1: ( f is being_homeomorphism & C c= Dp ) ; :: thesis: ( for p1, p2 being Point of I[01] holds
( not p1 < p2 or not f .: C = [.p1,p2.] ) or ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 )
given p1, p2 being Point of I[01] such that A2: ( p1 < p2 & f .: C = [.p1,p2.] ) ; :: thesis: ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
reconsider E = [.p1,p2.] as Subset of I(01) by A2;
set g = (f " ) | E;
f " is being_homeomorphism by A1, TOPS_2:70;
then A3: f " is one-to-one by TOPS_2:def 5;
A4: ( f is continuous & f is one-to-one ) by A1, TOPS_2:def 5;
A5: f " (f .: C) = C

proof

thus f " (f .: C) c= C by A4, FUNCT_1:152; :: according to XBOOLE_0:def 10 :: thesis: C c= f " (f .: C)
dom f = the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:def 1;
then C c= dom f by A1, PRE_TOPC:29;
hence C c= f " (f .: C) by FUNCT_1:146; :: thesis: verum

end;

A6: rng f = [#] I(01) by A1, TOPS_2:def 5;
then A7: (f " ) .: E = C by A2, A4, A5, TOPS_2:68;
A8: rng ((f " ) | E) = (f " ) .: E by RELAT_1:148
.= [#] ((TOP-REAL 2) | C) by A7, PRE_TOPC:29 ;
the carrier of (I(01) | E) = E by PRE_TOPC:29;
then (f " ) | E is Function of the carrier of (I(01) | E),the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:38;
then reconsider g = (f " ) | E as Function of (I(01) | E),((TOP-REAL 2) | C) by A8, FUNCT_2:8;
dom (f " ) = the carrier of I(01) by FUNCT_2:def 1;
then dom g = E by RELAT_1:91
.= the carrier of (I(01) | E) by PRE_TOPC:29 ;
then A9: dom g = [#] (I(01) | E) ;
A10: g is one-to-one by A3, FUNCT_1:84;
( the carrier of ((TOP-REAL 2) | C) = C & the carrier of ((TOP-REAL 2) | Dp) = Dp ) by PRE_TOPC:29;
then A11: (TOP-REAL 2) | C is SubSpace of (TOP-REAL 2) | Dp by A1, TOPMETR:4;
f " is continuous by A1, TOPS_2:def 5;
then A12: g is continuous by A11, Th69;
A13: g " = g " by A8, A10, TOPS_2:def 4
.= ((f " ) " ) | ((f " ) .: E) by A3, RFUNCT_2:40
.= ((f " ) " ) | ((f " ) .: E) by A4, A6, TOPS_2:def 4
.= f | C by A4, A7, FUNCT_1:65 ;
then reconsider t = f | C as Function of ((TOP-REAL 2) | C),(I(01) | E) ;
reconsider C' = C as Subset of ((TOP-REAL 2) | Dp) by A1, PRE_TOPC:29;
((TOP-REAL 2) | Dp) | C' = (TOP-REAL 2) | C by A1, PRE_TOPC:28;
then t is continuous by A4, Th69;
then g is being_homeomorphism by A8, A9, A10, A12, A13, TOPS_2:def 5;
then I(01) | E,(TOP-REAL 2) | C are_homeomorphic by T_0TOPSP:def 1;
hence ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 by A2, Th79; :: thesis: verum