let C be Simple_closed_curve; for U being Subset of ((TOP-REAL 2) | (C `)) st U is a_component holds
((TOP-REAL 2) | (C `)) | U is pathwise_connected
let U be Subset of ((TOP-REAL 2) | (C `)); ( U is a_component implies ((TOP-REAL 2) | (C `)) | U is pathwise_connected )
set T = (TOP-REAL 2) | (C `);
assume A1:
U is a_component
; ((TOP-REAL 2) | (C `)) | U is pathwise_connected
let a, b be Point of (((TOP-REAL 2) | (C `)) | U); BORSUK_2:def 3 a,b are_connected
A2:
the carrier of (((TOP-REAL 2) | (C `)) | U) = U
by PRE_TOPC:8;
A3:
U <> {} ((TOP-REAL 2) | (C `))
by A1, CONNSP_1:32;
per cases
( a = b or a <> b )
;
suppose A5:
a <> b
;
a,b are_connected A6:
((TOP-REAL 2) | (C `)) | U is
SubSpace of
TOP-REAL 2
by TSEP_1:7;
then reconsider a1 =
a,
b1 =
b as
Point of
(TOP-REAL 2) by A3, PRE_TOPC:25;
reconsider V =
U as
Subset of
(TOP-REAL 2) by PRE_TOPC:11;
V is_a_component_of C `
by A1;
then A7:
V is
open
by SPRECT_3:8;
U is
connected
by A1;
then
V is
connected
by CONNSP_1:23;
then consider P being
Subset of
(TOP-REAL 2) such that A8:
P is_S-P_arc_joining a1,
b1
and A9:
P c= V
by A2, A3, A5, A7, TOPREAL4:29;
A10:
a1 in P
by A8, TOPREAL4:3;
P is_an_arc_of a1,
b1
by A8, TOPREAL4:2;
then consider g being
Function of
I[01],
((TOP-REAL 2) | P) such that A11:
g is
being_homeomorphism
and A12:
g . 0 = a
and A13:
g . 1
= b
by TOPREAL1:def 1;
A14:
the
carrier of
((TOP-REAL 2) | P) = P
by PRE_TOPC:8;
then reconsider f =
g as
Function of
I[01],
(((TOP-REAL 2) | (C `)) | U) by A2, A9, A10, FUNCT_2:7;
take
f
;
BORSUK_2:def 1 ( f is continuous & f . 0 = a & f . 1 = b )
(TOP-REAL 2) | P is
SubSpace of
((TOP-REAL 2) | (C `)) | U
by A2, A6, A9, A14, TSEP_1:4;
hence
f is
continuous
by A11, PRE_TOPC:26;
( f . 0 = a & f . 1 = b )thus
(
f . 0 = a &
f . 1
= b )
by A12, A13;
verum end;