let n be 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
P is_an_arc_of p2,p1
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
P is_an_arc_of p2,p1
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies P is_an_arc_of p2,p1 )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: P is_an_arc_of p2,p1
then consider f being Function of I[01],((TOP-REAL n) | P) such that
A2: f is being_homeomorphism and
A3: f . 0 = p1 and
A4: f . 1 = p2 by TOPREAL1:def 1;
set Ex = L[01] (((0,1) (#)),((#) (0,1)));
A5: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;
set g = f * (L[01] (((0,1) (#)),((#) (0,1))));
A6: (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def 14, TREAL_1:5, TREAL_1:9;
A7: (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def 15, TREAL_1:5, TREAL_1:9;
dom f = [#] I[01] by A2, TOPS_2:def 5;
then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A5, TOPMETR:20, TOPS_2:def 5;
then A8: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;
reconsider P = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;
A9: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A5, A8, TOPMETR:20, TOPS_2:def 5;
reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL n) | P) by TOPMETR:20;
A10: g is being_homeomorphism by A2, A5, TOPMETR:20, TOPS_2:57;
A11: g . 0 = p2 by A4, A7, A9, BORSUK_1:def 14, FUNCT_1:12, TREAL_1:5;
g . 1 = p1 by A3, A6, A9, BORSUK_1:def 15, FUNCT_1:12, TREAL_1:5;
hence P is_an_arc_of p2,p1 by A10, A11, TOPREAL1:def 1; :: thesis: verum