let C be Simple_closed_curve; :: thesis: for U being Subset of ((TOP-REAL 2) | (C ` )) st U is_a_component_of (TOP-REAL 2) | (C ` ) holds
((TOP-REAL 2) | (C ` )) | U is arcwise_connected
let U be Subset of ((TOP-REAL 2) | (C ` )); :: thesis: ( U is_a_component_of (TOP-REAL 2) | (C ` ) implies ((TOP-REAL 2) | (C ` )) | U is arcwise_connected )
set T = (TOP-REAL 2) | (C ` );
assume A1:
U is_a_component_of (TOP-REAL 2) | (C ` )
; :: thesis: ((TOP-REAL 2) | (C ` )) | U is arcwise_connected
let a, b be Point of (((TOP-REAL 2) | (C ` )) | U); :: according to BORSUK_2:def 3 :: thesis: a,b are_connected
A2:
the carrier of (((TOP-REAL 2) | (C ` )) | U) = U
by PRE_TOPC:29;
A3:
U <> {} ((TOP-REAL 2) | (C ` ))
by A1, CONNSP_1:34;
then A4:
not ((TOP-REAL 2) | (C ` )) | U is empty
;
per cases
( a = b or a <> b )
;
suppose A6:
a <> b
;
:: thesis: a,b are_connected A7:
((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 A4, PRE_TOPC:55;
reconsider V =
U as
Subset of
(TOP-REAL 2) by PRE_TOPC:39;
V is_a_component_of C `
by A1, CONNSP_1:def 6;
then A8:
V is
open
by SPRECT_3:18;
U is
connected
by A1, CONNSP_1:def 5;
then
V is
connected
by CONNSP_1:24;
then
V is
being_Region
by A8;
then consider P being
Subset of
(TOP-REAL 2) such that A9:
P is_S-P_arc_joining a1,
b1
and A10:
P c= V
by A2, A3, A6, TOPREAL4:30;
A11:
a1 in P
by A9, TOPREAL4:4;
P is_an_arc_of a1,
b1
by A9, TOPREAL4:3;
then consider g being
Function of
I[01] ,
((TOP-REAL 2) | P) such that A12:
g is
being_homeomorphism
and A13:
(
g . 0 = a &
g . 1
= b )
by TOPREAL1:def 2;
A14:
the
carrier of
((TOP-REAL 2) | P) = P
by PRE_TOPC:29;
then reconsider f =
g as
Function of
I[01] ,
(((TOP-REAL 2) | (C ` )) | U) by A2, A10, A11, FUNCT_2:9;
take
f
;
:: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )A15:
g is
continuous
by A12;
(TOP-REAL 2) | P is
SubSpace of
((TOP-REAL 2) | (C ` )) | U
by A2, A7, A10, A14, TSEP_1:4;
hence
f is
continuous
by A15, PRE_TOPC:56;
:: thesis: ( f . 0 = a & f . 1 = b )thus
(
f . 0 = a &
f . 1
= b )
by A13;
:: thesis: verum end;