let n be Nat; 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); 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); ( P is_an_arc_of p1,p2 implies p1 <> p2 )
assume
P is_an_arc_of p1,p2
; p1 <> p2
then consider f being Function of I[01],((TOP-REAL n) | P) such that
A1:
f is being_homeomorphism
and
A2:
f . 0 = p1
and
A3:
f . 1 = p2
by TOPREAL1:def 1;
1 in [#] I[01]
by BORSUK_1:40, XXREAL_1:1;
then A4:
1 in dom f
by A1, TOPS_2:def 5;
A5:
f is one-to-one
by A1, TOPS_2:def 5;
0 in [#] I[01]
by BORSUK_1:40, XXREAL_1:1;
then
0 in dom f
by A1, TOPS_2:def 5;
hence
p1 <> p2
by A2, A3, A4, A5, FUNCT_1:def 4; verum