let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 holds
ex f being Path of q1,q2 st
( rng f c= P & rng f misses {p1,p2} )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 implies ex f being Path of q1,q2 st
( rng f c= P & rng f misses {p1,p2} ) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: ( q1 in P & q2 in P ) and
A3: ( q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 ) ; :: thesis: ex f being Path of q1,q2 st
( rng f c= P & rng f misses {p1,p2} )

per cases ( q1 = q2 or q1 <> q2 ) ;

suppose q1 = q2 ; :: thesis: ex f being Path of q1,q2 st
( rng f c= P & rng f misses {p1,p2} )

then reconsider f = I[01] --> q1 as Path of q1,q2 by Th41;
take f ; :: thesis: ( rng f c= P & rng f misses {p1,p2} )
A4: rng f = {q1} by FUNCOP_1:14;
thus rng f c= P :: thesis: rng f misses {p1,p2}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in P )
assume x in rng f ; :: thesis: x in P
hence x in P by A2, A4, TARSKI:def 1; :: thesis: verum

end;

( not p1 in {q1} & not p2 in {q1} ) by A3, TARSKI:def 1;
hence rng f misses {p1,p2} by A4, ZFMISC_1:57; :: thesis: verum

end;

suppose q1 <> q2 ; :: thesis: ex f being Path of q1,q2 st
( rng f c= P & rng f misses {p1,p2} )

then consider Q being non empty Subset of (TOP-REAL 2) such that
A5: Q is_an_arc_of q1,q2 and
A6: ( Q c= P & Q misses {p1,p2} ) by A1, A2, A3, JORDAN16:38;
consider g being Path of q1,q2, f being Function of I[01] ,((TOP-REAL 2) | Q) such that
A7: ( rng f = Q & g = f ) by A5, Th42;
reconsider h = f as Function of I[01] ,(TOP-REAL 2) by TOPREALA:28;
the carrier of ((TOP-REAL 2) | Q) = Q by PRE_TOPC:29;
then reconsider z1 = q1, z2 = q2 as Point of ((TOP-REAL 2) | Q) by A5, TOPREAL1:4;
A8: z1,z2 are_connected

proof

take f ; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = z1 & f . 1 = z2 )
thus f is continuous by A7, PRE_TOPC:57; :: thesis: ( f . 0 = z1 & f . 1 = z2 )
thus ( f . 0 = z1 & f . 1 = z2 ) by A7, BORSUK_2:def 4; :: thesis: verum

end;

f is Path of z1,z2

proof

thus z1,z2 are_connected by A8; :: according to BORSUK_2:def 2 :: thesis: ( f is continuous & f . 0 = z1 & f . 1 = z2 )
thus f is continuous by A7, PRE_TOPC:57; :: thesis: ( f . 0 = z1 & f . 1 = z2 )
thus ( f . 0 = z1 & f . 1 = z2 ) by A7, BORSUK_2:def 4; :: thesis: verum

end;

then reconsider h = h as Path of q1,q2 by A8, TOPALG_2:1;
take h ; :: thesis: ( rng h c= P & rng h misses {p1,p2} )
thus ( rng h c= P & rng h misses {p1,p2} ) by A6, A7; :: thesis: verum

end;

end;