let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
p1 <> p2
let P be Subset of (TOP-REAL n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
p1 <> p2
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies p1 <> p2 )
assume P is_an_arc_of p1,p2 ; :: thesis: p1 <> p2
then consider f being Function of I[01] ,((TOP-REAL n) | P) such that
A1: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by TOPREAL1:def 2;
1 in [#] I[01] by BORSUK_1:83, XXREAL_1:1;
then A2: 1 in dom f by A1, TOPS_2:def 5;
A3: f is one-to-one by A1, TOPS_2:def 5;
0 in [#] I[01] by BORSUK_1:83, XXREAL_1:1;
then 0 in dom f by A1, TOPS_2:def 5;
hence p1 <> p2 by A1, A2, A3, FUNCT_1:def 8; :: thesis: verum