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 connected

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 connected

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies P is connected )

assume A1: P is_an_arc_of p1,p2 ; :: thesis: P is connected

then consider f being Function of I[01],((TOP-REAL n) | P) such that

A2: f is being_homeomorphism and

f . 0 = p1 and

f . 1 = p2 by TOPREAL1:def 1;

reconsider P9 = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;

A3: f is continuous Function of I[01],((TOP-REAL n) | P9) by A2, TOPS_2:def 5;

A4: [#] I[01] is connected by CONNSP_1:27, TREAL_1:19;

A5: rng f = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def 5;

A6: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;

dom f = [#] I[01] by A2, TOPS_2:def 5;

then A7: P = f .: ([#] I[01]) by A5, A6, RELAT_1:113;

f .: ([#] I[01]) is connected by A3, A4, TOPS_2:61;

hence P is connected by A7, CONNSP_1:23; :: thesis: verum

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

P is connected

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 connected

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies P is connected )

assume A1: P is_an_arc_of p1,p2 ; :: thesis: P is connected

then consider f being Function of I[01],((TOP-REAL n) | P) such that

A2: f is being_homeomorphism and

f . 0 = p1 and

f . 1 = p2 by TOPREAL1:def 1;

reconsider P9 = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;

A3: f is continuous Function of I[01],((TOP-REAL n) | P9) by A2, TOPS_2:def 5;

A4: [#] I[01] is connected by CONNSP_1:27, TREAL_1:19;

A5: rng f = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def 5;

A6: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;

dom f = [#] I[01] by A2, TOPS_2:def 5;

then A7: P = f .: ([#] I[01]) by A5, A6, RELAT_1:113;

f .: ([#] I[01]) is connected by A3, A4, TOPS_2:61;

hence P is connected by A7, CONNSP_1:23; :: thesis: verum