let P be Subset of (TOP-REAL 2); 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); ( 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
and
A3:
q2 in P
and
A4:
q1 <> p1
and
A5:
q1 <> p2
and
A6:
q2 <> p1
and
A7:
q2 <> p2
; 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
;
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
;
( rng f c= P & rng f misses {p1,p2} )A8:
rng f = {q1}
by FUNCOP_1:8;
thus
rng f c= P
by A2, A8, TARSKI:def 1;
rng f misses {p1,p2}A9:
not
p1 in {q1}
by A4, TARSKI:def 1;
not
p2 in {q1}
by A5, TARSKI:def 1;
hence
rng f misses {p1,p2}
by A8, A9, ZFMISC_1:51;
verum end; suppose
q1 <> q2
;
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 A10:
Q is_an_arc_of q1,
q2
and A11:
Q c= P
and A12:
Q misses {p1,p2}
by A1, A2, A3, A4, A5, A6, A7, JORDAN16:23;
consider g being
Path of
q1,
q2,
f being
Function of
I[01],
((TOP-REAL 2) | Q) such that A13:
rng f = Q
and A14:
g = f
by A10, Th42;
reconsider h =
f as
Function of
I[01],
(TOP-REAL 2) by TOPREALA:7;
the
carrier of
((TOP-REAL 2) | Q) = Q
by PRE_TOPC:8;
then reconsider z1 =
q1,
z2 =
q2 as
Point of
((TOP-REAL 2) | Q) by A10, TOPREAL1:1;
A15:
z1,
z2 are_connected
A16:
f is
continuous
by A14, PRE_TOPC:27;
(
f . 0 = z1 &
f . 1
= z2 )
by A14, BORSUK_2:def 4;
then
f is
Path of
z1,
z2
by A15, A16, BORSUK_2:def 2;
then reconsider h =
h as
Path of
q1,
q2 by A15, TOPALG_2:1;
take
h
;
( rng h c= P & rng h misses {p1,p2} )thus
(
rng h c= P &
rng h misses {p1,p2} )
by A11, A12, A13;
verum end;