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

ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> 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

ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> p2 )

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> p2 ) )

assume P is_an_arc_of p1,p2 ; :: thesis: ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> 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 / 2 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;

then A4: 1 / 2 in dom f by A1, TOPS_2:def 5;

then f . (1 / 2) in rng f by FUNCT_1:def 3;

then f . (1 / 2) in the carrier of ((TOP-REAL n) | P) ;

then A5: f . (1 / 2) in P by PRE_TOPC:8;

then reconsider p = f . (1 / 2) as Point of (TOP-REAL n) ;

A6: 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;

then A7: p1 <> p by A2, A4, A6, FUNCT_1:def 4;

1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;

then 1 in dom f by A1, TOPS_2:def 5;

then f . 1 <> f . (1 / 2) by A4, A6, FUNCT_1:def 4;

hence ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> p2 ) by A3, A5, A7; :: thesis: verum

for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds

ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> 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

ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> p2 )

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> p2 ) )

assume P is_an_arc_of p1,p2 ; :: thesis: ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> 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 / 2 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;

then A4: 1 / 2 in dom f by A1, TOPS_2:def 5;

then f . (1 / 2) in rng f by FUNCT_1:def 3;

then f . (1 / 2) in the carrier of ((TOP-REAL n) | P) ;

then A5: f . (1 / 2) in P by PRE_TOPC:8;

then reconsider p = f . (1 / 2) as Point of (TOP-REAL n) ;

A6: 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;

then A7: p1 <> p by A2, A4, A6, FUNCT_1:def 4;

1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;

then 1 in dom f by A1, TOPS_2:def 5;

then f . 1 <> f . (1 / 2) by A4, A6, FUNCT_1:def 4;

hence ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> p2 ) by A3, A5, A7; :: thesis: verum