let T be TopSpace; :: thesis: for P being Subset of T
for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds
( p1 in P & p2 in P )
let P be Subset of T; :: thesis: for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds
( p1 in P & p2 in P )
let p1, p2 be Point of T; :: thesis: ( P is_an_arc_of p1,p2 implies ( p1 in P & p2 in P ) )
assume P is_an_arc_of p1,p2 ; :: thesis: ( p1 in P & p2 in P )
then consider f being Function of I[01],(T | P) such that
A1: f is being_homeomorphism and
A2: f . 0 = p1 and
A3: f . 1 = p2 ;
A4: dom f = [#] I[01] by A1, TOPS_2:def 5
.= the carrier of I[01] ;
1 in [.0,1.] by XXREAL_1:1;
then A5: p2 in rng f by A3, A4, BORSUK_1:40, FUNCT_1:def 3;
A6: rng f = [#] (T | P) by A1, TOPS_2:def 5;
0 in [.0,1.] by XXREAL_1:1;
then p1 in rng f by A2, A4, BORSUK_1:40, FUNCT_1:def 3;
hence ( p1 in P & p2 in P ) by A5, A6, PRE_TOPC:def 5; :: thesis: verum