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