let n be Element of NAT ; :: thesis: for D being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I[01] ,(TOP-REAL n) | D are_homeomorphic
let D be Subset of (TOP-REAL n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I[01] ,(TOP-REAL n) | D are_homeomorphic
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( D is_an_arc_of p1,p2 implies I[01] ,(TOP-REAL n) | D are_homeomorphic )
assume D is_an_arc_of p1,p2 ; :: thesis: I[01] ,(TOP-REAL n) | D are_homeomorphic
then ex f being Function of I[01],((TOP-REAL n) | D) st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by TOPREAL1:def 1;
hence I[01] ,(TOP-REAL n) | D are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum