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
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 2;
set Ex = L[01] (0 ,1 (#) ),((#) 0 ,1);
A5: L[01] (0 ,1 (#) ),((#) 0 ,1) is being_homeomorphism by TREAL_1:21;
set g = f * (L[01] (0 ,1 (#) ),((#) 0 ,1));
A6: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . (0 ,1 (#) ) = 0 by BORSUK_1:def 17, TREAL_1:8, TREAL_1:12;
A7: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . ((#) 0 ,1) = 1 by BORSUK_1:def 18, TREAL_1:8, TREAL_1:12;
dom f = [#] I[01] by A2, TOPS_2:def 5;
then rng (L[01] (0 ,1 (#) ),((#) 0 ,1)) = dom f by A5, TOPMETR:27, TOPS_2:def 5;
then A8: dom (f * (L[01] (0 ,1 (#) ),((#) 0 ,1))) = dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by RELAT_1:46;
reconsider P = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:4;
A9: dom (f * (L[01] (0 ,1 (#) ),((#) 0 ,1))) = [#] I[01] by A5, A8, TOPMETR:27, TOPS_2:def 5;
reconsider g = f * (L[01] (0 ,1 (#) ),((#) 0 ,1)) as Function of I[01] ,((TOP-REAL n) | P) by TOPMETR:27;
A10: g is being_homeomorphism by A2, A5, TOPMETR:27, TOPS_2:71;
A11: g . 0 = p2 by A4, A7, A9, BORSUK_1:def 17, FUNCT_1:22, TREAL_1:8;
g . 1 = p1 by A3, A6, A9, BORSUK_1:def 18, FUNCT_1:22, TREAL_1:8;
hence P is_an_arc_of p2,p1 by A10, A11, TOPREAL1:def 2; :: thesis: verum