let n be Element of NAT ; :: thesis: for C being non empty Subset of (TOP-REAL n)
for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) & I(01) | E,(TOP-REAL n) | C are_homeomorphic holds
ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
let C be non empty Subset of (TOP-REAL n); :: thesis: for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) & I(01) | E,(TOP-REAL n) | C are_homeomorphic holds
ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
let E be Subset of I(01); :: thesis: ( ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) & I(01) | E,(TOP-REAL n) | C are_homeomorphic implies ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2 )
given p1, p2 being Point of I[01] such that A1: p1 < p2 and
A2: E = [.p1,p2.] ; :: thesis: ( not I(01) | E,(TOP-REAL n) | C are_homeomorphic or ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2 )
A3: I[01] ,I(01) | E are_homeomorphic by A1, A2, Th67;
assume A4: I(01) | E,(TOP-REAL n) | C are_homeomorphic ; :: thesis: ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
not E is empty by A1, A2, Th49;
then I[01] ,(TOP-REAL n) | C are_homeomorphic by A4, A3, BORSUK_3:3;
then consider g being Function of I[01],((TOP-REAL n) | C) such that
A5: g is being_homeomorphism by T_0TOPSP:def 1;
set s1 = g . 0;
set s2 = g . 1;
0 in the carrier of I[01] by BORSUK_1:43;
then A6: g . 0 in the carrier of ((TOP-REAL n) | C) by FUNCT_2:5;
1 in the carrier of I[01] by BORSUK_1:43;
then A7: g . 1 in the carrier of ((TOP-REAL n) | C) by FUNCT_2:5;
the carrier of ((TOP-REAL n) | C) c= the carrier of (TOP-REAL n) by BORSUK_1:1;
then reconsider s1 = g . 0, s2 = g . 1 as Point of (TOP-REAL n) by A6, A7;
C is_an_arc_of s1,s2 by A5, TOPREAL1:def 1;
hence ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2 ; :: thesis: verum